Skip to content

Commit

Permalink
refactoring of distributions - probably too aggresive and should be r…
Browse files Browse the repository at this point in the history 
…everted
  • Loading branch information
@lecopivo
lecopivo committed Apr 1, 2024
1 parent 4af1c95 commit b87d1bf
Show file tree
Hide file tree
Showing 9 changed files with 378 additions and 380 deletions.
397 changes: 178 additions & 219 deletions SciLean/Core/Distribution/Basic.lean
View file

Large diffs are not rendered by default.

45 changes: 26 additions & 19 deletions SciLean/Core/Distribution/Eval.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ namespace SciLean

variable
{R} [RealScalar R]
{X} [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)]
{Y} [Vec R Y]
{X} [Vec R X] -- [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)]
{Y} [Vec R Y] [Module ℝ Y]
{Z} [Vec R Z]
{U} [Vec R U]
{V} [Vec R V]
{V} [Vec R V] [Module ℝ V]
{W} [Vec R W]

set_default_scalar R
Expand All @@ -21,48 +21,55 @@ open Classical

@[action_push]
theorem action_extAction (T : 𝒟' X) (φ : 𝒟 X) :
T.action φ = T.extAction φ := sorry_proof
T φ = T.extAction' φ := sorry_proof

@[action_push]
theorem extAction_vecDirac (x : X) (φ : X → R) :
(dirac x).extAction φ
theorem extAction_vecDirac (x : X) (φ : X → Y) (L : R ⊸ Y ⊸ Z) :
(dirac x).extAction φ L
=
φ x := sorry_proof
L 1 (φ x) := sorry_proof

@[action_push]
theorem extAction_restrict_vecDirac (x : X) (A : Set X) (φ : X → R) :
((dirac x).restrict A).extAction φ
theorem extAction_restrict_vecDirac (x : X) (A : Set X) (φ : X → Y) (L : R ⊸ Y ⊸ Z) :
((dirac x).restrict A).extAction φ L
=
if x ∈ A then φ x else 0 := sorry_proof
if x ∈ A then L 1 (φ x) else 0 := sorry_proof

-- x.postComp (fun u => (y u).extAction φ) := by sorry_proof

@[action_push]
theorem postExtAction_postComp (x : 𝒟'(X,U)) (y : U → 𝒟'(Y,Z)) (φ : Y → R) :
(x.postComp y).postExtAction φ
theorem postExtAction_postComp (x : 𝒟'(X,U)) (y : U ⊸ 𝒟'(Y,Z)) (φ : Y → R) :
(x.postComp y).postComp (⟨fun T => T.extAction' φ, by unfold Distribution.extAction'; fun_prop⟩)
=
x.postComp (fun u => (y u).extAction φ) := by sorry_proof
x.postComp (⟨fun u => (y u).extAction' φ, by unfold Distribution.extAction'; fun_prop⟩) := by sorry_proof

variable [MeasureSpace X]

open Rand in
@[action_push]
theorem function_toDistribution_eval (f : X → R) (A : Set X) (φ : X → R) [UniformRand A] :
(f.toDistribution.restrict A).extAction φ
theorem function_toDistribution_eval (f : X → Y) (A : Set X) (φ : X → U) (L : Y ⊸ U ⊸ V) [UniformRand A] :
(f.toDistribution.restrict A).extAction φ L
=
(uniform A).E fun x =>
let V : R := Scalar.ofENNReal (volume A)
V • f x * φ x := sorry_proof
V • L (f x) (φ x) := sorry_proof


open Rand in
@[action_push]
theorem function_toDistribution_eval_restrict (f : X → R) (B A : Set X) (φ : X → R) [UniformRand A] :
((f.toDistribution.restrict B).restrict A).extAction φ
theorem function_toDistribution_eval_restrict (f : X → Y) (B A : Set X) (φ : X → U) (L : Y ⊸ U ⊸ V) [UniformRand A] :
((f.toDistribution.restrict B).restrict A).extAction φ L
=
(uniform A).E fun x =>
let V : R := Scalar.ofENNReal (volume A)
if x.1 ∈ B then
V • f x * φ x
V • L (f x) (φ x)
else
0 := sorry_proof


@[simp, ftrans_simp, action_push]
theorem function_toDistribution_extAction_unit {X} [Vec R X] [Module ℝ X] (f : Unit → X) (φ : Unit → Y) (L : X ⊸ Y ⊸ Z) :
f.toDistribution.extAction φ L
=
L (f ()) (φ ()) := sorry_proof
99 changes: 60 additions & 39 deletions SciLean/Core/Distribution/ParametricDistribDeriv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,24 +17,25 @@ variable
{Y} [Vec R Y] [Module ℝ Y]
{Z} [Vec R Z] [Module ℝ Z]
{U} [Vec R U] -- [Module ℝ U]
{V} [Vec R V] -- [Module ℝ U]


set_default_scalar R


noncomputable
def diracDeriv (x dx : X) : 𝒟' X := ⟨fun φ ⊸ cderiv R φ x dx⟩
def diracDeriv (x dx : X) : 𝒟' X := fun φ ⊸ cderiv R φ x dx

@[fun_prop]
def DistribDifferentiableAt (f : X → 𝒟'(Y,Z)) (x : X) :=
∀ (φ : X → 𝒟 Y), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => ⟪f x, φ x⟫) x
∀ (φ : X → 𝒟 Y), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => f x (φ x)) x


theorem distribDifferentiableAt_const_test_fun
{f : X → 𝒟'(Y,Z)} {x : X}
(hf : DistribDifferentiableAt f x)
{φ : 𝒟 Y} :
CDifferentiableAt R (fun x => ⟪f x, φ⟫) x := by
CDifferentiableAt R (fun x => f x φ) x := by
apply hf
fun_prop

Expand All @@ -57,12 +58,12 @@ open Classical in
@[fun_trans]
noncomputable
def parDistribDeriv (f : X → 𝒟'(Y,Z)) (x dx : X) : 𝒟'(Y,Z) :=
⟨⟨fun φ => ∂ (x':=x;dx), ⟪f x', φ⟫, sorry_proof⟩⟩
⟨fun φ => ∂ (x':=x;dx), f x' φ, sorry_proof⟩


@[simp, ftrans_simp]
theorem action_parDistribDeriv (f : X → 𝒟'(Y,Z)) (x dx : X) (φ : 𝒟 Y) :
⟪parDistribDeriv f x dx, φ⟫ = ∂ (x':=x;dx), ⟪f x', φ⟫ := rfl
parDistribDeriv f x dx φ = ∂ (x':=x;dx), f x' φ := rfl


----------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -126,7 +127,7 @@ theorem DistribDiffrentiable.comp_rule
intro x
unfold DistribDifferentiableAt
intro φ hφ
apply CDifferentiable.comp_rule (K:=R) (f:=fun xy : X×Y => ⟪f xy.2,φ xy.1⟫) (g:=fun x => (x, g x))
apply CDifferentiable.comp_rule (K:=R) (f:=fun xy : X×Y => f xy.2 (φ xy.1)) (g:=fun x => (x, g x))
(hg:=by fun_prop)
intro x
sorry_proof -- is this even true ?
Expand Down Expand Up @@ -157,10 +158,10 @@ theorem parDistribDeriv.comp_rule
-- I think `f` has to be `deg`
@[fun_prop]
theorem Bind.bind.arg_fx.DistribDifferentiable_rule
(f : X → Y → 𝒟' Z) (g : X → 𝒟' Y)
(f : X → Y → 𝒟'(Z,V)) (g : X → 𝒟'(Y,U)) (L : U ⊸ V ⊸ W)
(hf : DistribDifferentiable (fun (x,y) => f x y)) -- `f` has to be nice enough to accomodate action of `g`
(hg : DistribDifferentiable g) :
DistribDifferentiable (fun x => (g x).bind (f x)) := by
DistribDifferentiable (fun x => (g x).bind (f x) L) := by

intro x
unfold DistribDifferentiableAt
Expand All @@ -171,15 +172,15 @@ theorem Bind.bind.arg_fx.DistribDifferentiable_rule

@[fun_trans]
theorem Bind.bind.arg_fx.parDistribDiff_rule
(f : X → Y → 𝒟' Z) (g : X → 𝒟' Y)
(f : X → Y → 𝒟'(Z,V)) (g : X → 𝒟'(Y,U)) (L : U ⊸ V ⊸ W)
(hf : DistribDifferentiable (fun (x,y) => f x y)) -- `f` has to be nice enough to accomodate action of `g`
(hg : DistribDifferentiable g) :
parDistribDeriv (fun x => (g x).bind (f x))
parDistribDeriv (fun x => (g x).bind (f x) L)
=
fun x dx =>
((parDistribDeriv g x dx).bind (f x · ))
((parDistribDeriv g x dx).bind (f x · ) L)
+
((g x).bind (fun y => parDistribDeriv (f · y) x dx)) := sorry_proof
((g x).bind (fun y => parDistribDeriv (f · y) x dx) L) := sorry_proof



Expand Down Expand Up @@ -217,11 +218,11 @@ theorem toDistribution.linear_parDistribDeriv_rule (f : W → X → Y) (L : Y
parDistribDeriv (fun w => (fun x => L (f w x)).toDistribution)
=
fun w dw =>
parDistribDeriv Tf w dw |>.postComp L := by
parDistribDeriv (fun w => (fun x => f w x).toDistribution) w dw |>.postComp (fun y ⊸ L y) := by
funext w dw
unfold parDistribDeriv Distribution.postComp Function.toDistribution
ext φ
simp [ftrans_simp, Distribution.mk_extAction_simproc]
simp [ftrans_simp] -- , Distribution.mk_extAction_simproc]
sorry_proof


Expand All @@ -235,45 +236,42 @@ variable [MeasureSpace X] [MeasureSpace Y] [MeasureSpace (X×Y)]
open Notation

@[fun_trans]
theorem cintegral.arg_f.cderiv_distrib_rule (f : W → X → R) :
theorem cintegral.arg_f.cderiv_distrib_rule (f : W → X → Y) :
cderiv R (fun w => ∫' x, f w x)
=
fun w dw =>
(parDistribDeriv (fun w => (f w ·).toDistribution) w dw).extAction (fun _ => 1) := sorry_proof
(parDistribDeriv (fun w => (f w ·).toDistribution) w dw).extAction (fun _ => (1:R)) (fun y ⊸ fun r ⊸ r • y) := sorry_proof


@[fun_trans]
theorem cintegral.arg_f.cderiv_distrib_rule' (f : W → X → R) (A : Set X):
cderiv R (fun w => ∫' x in A, f w x)
=
fun w dw =>
(parDistribDeriv (fun w => (f w ·).toDistribution) w dw).restrict A |>.extAction fun _ => 1 := sorry_proof

-- (parDistribDeriv (fun w => (f w ·).toDistribution) w dw).extAction (fun x => if x ∈ A then 1 else 0) := sorry_proof

(parDistribDeriv (fun w => (f w ·).toDistribution) w dw).restrict A |>.extAction (fun _ => (1:R)) (fun y ⊸ fun r ⊸ r • y) := sorry_proof


@[fun_trans]
theorem cintegral.arg_f.parDistribDeriv_rule (f : W → X → Y → R) :
parDistribDeriv (fun w => (fun x => ∫' y, f w x y).toDistribution)
theorem cintegral.arg_f.parDistribDeriv_rule (f : W → X → Y → Z) :
parDistribDeriv (fun w => (fun x => ∫' y, f w x y).toDistribution (R:=R))
=
fun w dw =>
let Tf := (fun w => (fun x => (fun y => f w x y).toDistribution (R:=R)).toDistribution (R:=R))
parDistribDeriv Tf w dw |>.postExtAction (fun _ => 1) := by
parDistribDeriv Tf w dw |>.postComp (fun T ⊸ T.extAction (fun _ => (1:R)) (fun z ⊸ fun r ⊸ r • z)) := by
funext w dw
unfold postExtAction parDistribDeriv postComp Function.toDistribution
unfold parDistribDeriv postComp Function.toDistribution
ext φ
simp [ftrans_simp, Distribution.mk_extAction_simproc]
simp [ftrans_simp] -- , Distribution.mk_extAction_simproc]
sorry_proof


@[fun_trans]
theorem cintegral.arg_f.parDistribDeriv_rule' (f : W → X → Y → R) (B : X → Set Y) :
theorem cintegral.arg_f.parDistribDeriv_rule' (f : W → X → Y → Z) (B : X → Set Y) :
parDistribDeriv (fun w => (fun x => ∫' y in B x, f w x y).toDistribution)
=
fun w dw =>
let Tf := (fun w => (fun x => ((fun y => f w x y).toDistribution (R:=R)).restrict (B x)).toDistribution (R:=R))
parDistribDeriv Tf w dw |>.postExtAction (fun _ => 1) := sorry_proof
parDistribDeriv Tf w dw |>.postComp (fun T ⊸ T.extAction (fun _ => (1:R)) (fun z ⊸ fun r ⊸ r • z)) := sorry_proof



Expand All @@ -284,21 +282,21 @@ theorem cintegral.arg_f.parDistribDeriv_rule' (f : W → X → Y → R) (B : X
----------------------------------------------------------------------------------------------------

@[fun_prop]
theorem HAdd.hAdd.arg_a0a1.DistribDifferentiable_rule (f g : W → X → R)
theorem HAdd.hAdd.arg_a0a1.DistribDifferentiable_rule (f g : W → X → Y)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
DistribDifferentiable (fun w => (fun x => f w x + g w x).toDistribution) := by
DistribDifferentiable (fun w => (fun x => f w x + g w x).toDistribution (R:=R)) := by
intro _ φ hφ; simp; sorry_proof -- fun_prop (disch:=assumption)

-- we probably only require local integrability in `x` of f and g for this to be true
@[fun_trans]
theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W → X → R)
theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W → X → Y)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
parDistribDeriv (fun w => (fun x => f w x + g w x).toDistribution)
=
fun w dw =>
parDistribDeriv (fun w => (f w ·).toDistribution) w dw
+
parDistribDeriv (fun w => (g w ·).toDistribution) w dw := by
parDistribDeriv (fun w => (g w ·).toDistribution (R:=R)) w dw := by
funext w dw; ext φ; simp[parDistribDeriv]
sorry_proof

Expand All @@ -308,21 +306,21 @@ theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W → X → R)
----------------------------------------------------------------------------------------------------

@[fun_prop]
theorem HSub.hSub.arg_a0a1.DistribDifferentiable_rule (f g : W → X → R)
theorem HSub.hSub.arg_a0a1.DistribDifferentiable_rule (f g : W → X → Y)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
DistribDifferentiable (fun w => (fun x => f w x - g w x).toDistribution) := by
DistribDifferentiable (fun w => (fun x => f w x - g w x).toDistribution (R:=R)) := by
intro _ φ hφ; simp; sorry_proof -- fun_prop (disch:=assumption)


@[fun_trans]
theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W → X → R)
theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W → X → Y)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
parDistribDeriv (fun w => (fun x => f w x - g w x).toDistribution)
=
fun w dw =>
parDistribDeriv (fun w => (f w ·).toDistribution) w dw
-
parDistribDeriv (fun w => (g w ·).toDistribution) w dw := by
parDistribDeriv (fun w => (g w ·).toDistribution (R:=R)) w dw := by
funext w dw; ext φ; simp[parDistribDeriv]
sorry_proof

Expand All @@ -334,7 +332,7 @@ theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W → X → R)
@[fun_prop]
theorem HMul.hMul.arg_a0a1.DistribDifferentiable_rule (f : W → X → R) (r : R)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
DistribDifferentiable (fun w => (fun x => r * f w x).toDistribution) := by
DistribDifferentiable (fun w => (fun x => r * f w x).toDistribution (R:=R)) := by
intro _ φ hφ; simp; sorry_proof -- fun_prop (disch:=assumption)


Expand All @@ -344,19 +342,42 @@ theorem HMul.hMul.arg_a0a1.parDistribDeriv_rule (f : W → X → R) (r : R)
parDistribDeriv (fun w => (fun x => r * f w x).toDistribution)
=
fun w dw =>
r • (parDistribDeriv (fun w => (f w ·).toDistribution) w dw) := by
r • (parDistribDeriv (fun w => (f w ·).toDistribution (R:=R)) w dw) := by
funext w dw; ext φ; simp[parDistribDeriv]
sorry_proof


----------------------------------------------------------------------------------------------------
-- Smul ---------------------------------------------------------------------------------------------
----------------------------------------------------------------------------------------------------

@[fun_prop]
theorem HSMul.hSMul.arg_a0a1.DistribDifferentiable_rule (f : W → X → Y) (r : R)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
DistribDifferentiable (fun w => (fun x => r • f w x).toDistribution (R:=R)) := by
intro _ φ hφ; simp; sorry_proof -- fun_prop (disch:=assumption)


@[fun_trans]
theorem HSMul.hSMul.arg_a0a1.parDistribDeriv_rule (f : W → X → Y) (r : R)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
parDistribDeriv (fun w => (fun x => r • f w x).toDistribution)
=
fun w dw =>
r • (parDistribDeriv (fun w => (f w ·).toDistribution (R:=R)) w dw) := by
funext w dw; ext φ; simp[parDistribDeriv]
sorry_proof



----------------------------------------------------------------------------------------------------
-- Div ---------------------------------------------------------------------------------------------
----------------------------------------------------------------------------------------------------

@[fun_prop]
theorem HDiv.hDiv.arg_a0a1.DistribDifferentiable_rule (f : W → X → R) (r : R)
/- (hf : ∀ x, CDifferentiable R (f · x)) (hg : ∀ x, CDifferentiable R (g · x)) -/ :
DistribDifferentiable (fun w => (fun x => f w x / r).toDistribution) := by
DistribDifferentiable (fun w => (fun x => f w x / r).toDistribution (R:=R)) := by
intro _ φ hφ; simp; sorry_proof -- fun_prop (disch:=assumption)


Expand All @@ -366,6 +387,6 @@ theorem HDiv.hDiv.arg_a0a1.parDistribDeriv_rule (f : W → X → R) (r : R)
parDistribDeriv (fun w => (fun x => f w x / r).toDistribution)
=
fun w dw =>
r⁻¹ • (parDistribDeriv (fun w => (f w ·).toDistribution) w dw) := by
r⁻¹ • (parDistribDeriv (fun w => (f w ·).toDistribution (R:=R)) w dw) := by
funext w dw; ext φ; simp[parDistribDeriv]
sorry_proof
Loading

0 comments on commit b87d1bf

Please sign in to comment.