work on HasDerivUnderIntegral

SciLean/Core/Distribution/Basic.lean

@@ -622,6 +622,8 @@ def Distribution.toMeasure (f' : 𝒟' X) : Measure X :=
   else
     0
 
+
+
 -- @[simp]
 -- theorem apply_measure_as_distribution  {X} [MeasurableSpace X]  (μ : Measure X) (φ : X → Y) :
 --      ⟪μ.toDistribution, φ⟫ = ∫ x, φ x ∂μ := by rfl

SciLean/Core/Distribution/RestrictToLevelSet.lean

@@ -0,0 +1,92 @@
+import Mathlib.MeasureTheory.Decomposition.Lebesgue
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.MeasureTheory.Measure.VectorMeasure
+
+import SciLean.Core.Distribution.Basic
+import SciLean.Core.Integral.MovingDomain
+import SciLean.Core.Integral.VectorIntegral
+
+import SciLean.Core.Objects.Scalar
+
+namespace SciLean
+
+open MeasureTheory FiniteDimensional
+
+variable
+  {R} [RealScalar R] [MeasureSpace R]
+  {W} [Vec R W]
+  {X} [SemiHilbert R X] [MeasureSpace X]
+  {U} [Vec R U] [Module ℝ U]
+
+set_default_scalar R
+
+def Distribution.IsVectorMeasure (f : 𝒟'(X,U)) : Prop :=
+  ∃ (μ : VectorMeasure X U), ∀ (φ : 𝒟 X),
+      f φ = vectorIntegral (fun x => φ x) μ (fun u v => u•v)
+
+open Classical
+noncomputable
+def Distribution.toVectorMeasure (f' : 𝒟'(X,U)) : VectorMeasure X U :=
+  if h : f'.IsVectorMeasure then
+    choose h
+  else
+    0
+
+
+
+variable (R)
+
+
+/-- Given a familly of surfaces `S`, restrict `u` to the surface `S w`.
+
+It is necessary that the distribution `u` just an integrable function `f` i.e.
+`⟨u,φ⟩ = ∫ x, φ x • f x` -/
+noncomputable
+def Distribution.restrictToFrontier (u : 𝒟'(X,U)) (S : W → Set X) (w dw : W) : 𝒟'(X,U) :=
+  let s := fun x => (frontierSpeed R S w dw x)
+  let dudV := u.toFunction
+  fun φ ⊸ ∫' x in S w, (φ x * s x) • dudV x ∂(surfaceMeasure (finrank R X - 1))
+
+variable {R}
+
+
+
+
+/-- Restrict measure `μ` to `θ` level set of a function `φ` obtaining (n-1)-dimensional integral -/
+noncomputable
+def _root_.MeasureTheory.Measure.restrictToLevelSet (μ : Measure X) (φ : W → X → R) (w dw : W) :
+    VectorMeasure X R := μ.restrictToFrontier R (fun w => {x | φ w x ≤ 0}) w dw
+
+
+@[ftrans_simp]
+theorem restrictToFrontier_eq_restrictToLevelSet (μ : Measure X) (φ ψ : W → X → R) :
+  μ.restrictToFrontier R (fun w => {x | φ w x ≤ ψ w x})
+  =
+  μ.restrictToLevelSet (fun w x => φ w x - ψ w x) := sorry_proof
+
+
+-- /-- Volume integral can be split into integral over reals and level sets.
+
+--   TODO: add proper assumptions:
+--             - integrability of f
+--             - non-zero gradient of `φ` almost everywhere
+--             - `μ ≪ volume`
+-- -/
+-- theorem cintegral_cintegral_conditionOn (f : X → U) (φ : X → R) (μ : Measure X) :
+--     ∫' t, ∫' x, f x ∂(μ.restrictToLevelSet (fun t x => φ x - t) t)
+--     =
+--     ∫' x, f x ∂μ := sorry_proof
+
+
+
+-- /-- Derivative of integral over sub-levelsets is equal to the integral over level set.
+
+--   TODO: add proper assumptions:
+--             - integrability of f
+--             - non-zero gradient of `φ` almost everywhere
+--             - `μ ≪ volume`
+-- -/
+-- theorem cderiv_cintegral_in_level_set (f : X → U) (φ : W → X → R) (μ : Measure X) :
+--     (cderiv R fun w => ∫' x in {x | φ w x ≤ 0}, f x ∂μ)
+--     =
+--     fun w dw => dw • ∫' x, f x ∂(μ.restrictToLevelSet φ w dw) := sorry_proof

SciLean/Core/Integral/HasDerivUnderIntegral.lean

@@ -1,9 +1,11 @@
 import SciLean.Notation
-import SciLean.Core.Integral.CIntegral
-import SciLean.Core.Integral.Surface
 import SciLean.Core.FunctionTransformations
 import SciLean.Core.Notation
 
+import SciLean.Core.Integral.CIntegral
+import SciLean.Core.Integral.Surface
+import SciLean.Core.Integral.RestrictToLevelSet
+
 import SciLean.Tactic.GTrans
 
 import Mathlib.MeasureTheory.Decomposition.Lebesgue
@@ -222,11 +224,13 @@ theorem cintegral.arg_f.HasDerivUnderIntegral_rule
   (w : W) (f : W → X → Y → Z) (μ : Measure X) (ν : Measure Y)
   (f' : W → X×Y → Z) (sf : W → Z)
   (hf : HasDerivUnderIntegralAt R (fun w (xy : X×Y) => f w xy.1 xy.2) (μ.prod ν) w f' sf) :
-  HasDerivUnderIntegralAt R (fun w x => ∫' y, f w x y ∂ν) μ w (fun dw x => ∫' y, f' dw (x,y) ∂ν) sf := sorry_proof
+  HasDerivUnderIntegralAt R
+    (fun w x => ∫' y, f w x y ∂ν) μ w
+    (fun dw x => ∫' y, f' dw (x,y) ∂ν) sf := sorry_proof
 
 
 @[gtrans]
-theorem ite.arg_cte.HasDerivUnderIntegral_rule
+theorem ite.arg_cte.HasDerivUnderIntegral_rule {X} [SemiHilbert R X] [MeasureSpace X]
   (t e : W → X → Y) (μ : Measure X) (w : W)
   (c : W → X → Prop) [∀ w x, Decidable (c w x)]
   (t' e' : W → X → Y) (st se : W → Y)
@@ -237,7 +241,25 @@ theorem ite.arg_cte.HasDerivUnderIntegral_rule
     (fun w x => if c w x then t w x else e w x) μ w
     (fun dw x => if c w x then t' dw x else e' dw x)
     (fun dw =>
-       let ds := movingFrontierIntegral R (fun x => t w x - e w x) (fun w => {x | c w x}) μ w dw
+       let ds := vectorIntegral (fun x => (t w x - e w x)) (μ.restrictToFrontier R (fun w => {x | c w x}) w dw) (fun y r => r•y)
        let st' := st dw
        let se' := se dw
        st' + se' + ds) := sorry_proof
+
+
+-- @[gtrans]
+-- theorem ite.arg_cte.HasDerivUnderIntegral_rule {X} [SemiHilbert R X] [MeasureSpace X]
+--   (t e : W → X → Y) (μ : Measure X) (w : W)
+--   (φ ψ : W → X → R)
+--   (t' e' : W → X → Y) (st se : W → Y)
+--   -- (hμ : μ ≪ volume)
+--   (hf : HasDerivUnderIntegralAt R t (μ.restrict {x | φ w x ≤ ψ w x}) w t' st)
+--   (hg : HasDerivUnderIntegralAt R e (μ.restrict {x | φ w x ≤ ψ w x}ᶜ) w e' se) :
+--   HasDerivUnderIntegralAt R
+--     (fun w x => if φ w x ≤ ψ w x then t w x else e w x) μ w
+--     (fun dw x => if φ w x ≤ ψ w x then t' dw x else e' dw x)
+--     (fun dw =>
+--        let ds := ∫' x, (t w x - e w x) ∂(μ.restrictToLevelSet R (fun w x => φ w x - ψ w x) w dw x)
+--        let st' := st dw
+--        let se' := se dw
+--        st' + se' + ds) := sorry_proof

SciLean/Core/Integral/MovingDomain.lean

@@ -48,14 +48,12 @@ variable (R)
 open Classical in
 noncomputable
 def frontierSpeed (A : W → Set X) (w dw : W) (x : X) : R :=
-  -- todo: use some version of `IsLipschitzDomain` to get `φ`
-  sorry
-  -- if h : ∃ φ : W → X → R, ∀ w, A w = {x | 0 ≤ φ w x} then
-  --   let φ := choose h
-  --   -- TODO: turn `x` to the closes point on the boundary
-  --   levelSetSpeed φ w dw x
-  -- else
-  --   0
+  match Classical.dec (∃ (φ : W → X → R), (∀ w, A w = {x | φ w x = 0})) with
+  | .isTrue h =>
+    let φ := Classical.choose h
+    (-(∂ (w':=w;dw), φ w' x)/‖∇ x':=x, φ w x'‖₂)
+  | .isFalse _ => 0
+
 variable {R}
 
 
@@ -93,6 +91,8 @@ theorem moving_volume_derivative (f : W → X → Y) (A : W → Set X) (hA : IsL
 -- Moving Frontier Integral ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------------
 
+#exit
+
 variable (R)
 @[fun_trans]
 noncomputable
@@ -234,6 +234,7 @@ theorem cintegral.arg_fμ.cderiv_rule_add (f g : W → X → Y) (A : Set X) :
       ds + dy + dz := sorry_proof
 
 
+#exit
 
 variable (R)
 /-- -/

SciLean/Core/Integral/PlaneDecomposition.lean

@@ -39,7 +39,7 @@ def gramSchmidtDataArrayImpl {X} [SemiHilbert R X] [PlainDataType X] (u : X^[n])
   return u
 
 
-open IndexType Scalar in
+open IndexType Scalar FinVec in
 /-- Given a plane `{x | ⟪u,x⟫=0}` this function decomposes `R^[n]` into this plane and its
 orthogonal complement.
 

SciLean/Core/Integral/RestrictToLevelSet.lean

@@ -0,0 +1,118 @@
+import Mathlib.MeasureTheory.Decomposition.Lebesgue
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.MeasureTheory.Measure.VectorMeasure
+
+import SciLean.Core.Integral.Surface
+import SciLean.Core.Integral.MovingDomain
+import SciLean.Core.Integral.VectorIntegral
+
+import SciLean.Core.Objects.Scalar
+
+namespace SciLean
+
+open MeasureTheory FiniteDimensional
+
+variable
+  {R} [RealScalar R] [MeasureSpace R]
+  {W} [Vec R W]
+  {X} [SemiHilbert R X] [MeasureSpace X]
+  {U} [Vec R U] [Module ℝ U]
+
+set_default_scalar R
+
+
+-- /-- Given a family of surface `S`, compute the surface speed in the normal direction at point `x`
+--  and time `t`.
+
+-- TODO: Fix the definition if `x` is not a point on the surface `S t`.
+--       Possible return values are:
+--         - speed on the closes point
+--         - zero -/
+-- noncomputable
+-- def surfaceSpeed (S : R → Set X) (x : X) (t : R) : R :=
+--   -- 'if _ then _ else _' breaks where for some reason
+--   match Classical.dec (∃ (φ : X → R → R), (∀ t, S t = {x | φ x t = 0})) with
+--   | .isTrue h =>
+--     let φ := Classical.choose h
+--     (-(∂ (t':=t), φ x t')/‖∇ x':=x, φ x' t‖₂)
+--   | .isFalse _ => 0
+
+
+-- /-- Given a familly of surfaces `S`, restrict `μ` to the surface `S θ`.
+
+-- It is necessary that `μ` is absolutely continuous w.r.t. to Lebesgue measure and that `S` vary
+-- smoothly.  -/
+-- noncomputable
+-- def _root_.MeasureTheory.Measure.restrictToSurface (μ : Measure X) (S : R → Set X) (θ : R) :
+--     Measure X where
+--   measureOf := fun A =>
+--     let Dφ := fun x => Scalar.toENNReal (surfaceSpeed S x θ)
+--     let dμdV := μ.rnDeriv volume
+--     ∫⁻ x in A ∩ S θ, Dφ x * dμdV x ∂(surfaceMeasure (finrank R X - 1))
+--   empty := sorry_proof
+--   mono := sorry_proof
+--   iUnion_nat := sorry_proof
+--   m_iUnion := sorry_proof
+--   trimmed := sorry_proof
+
+
+
+variable (R)
+
+/-- Given a familly of surfaces `S`, restrict `μ` to the surface `S w`.
+
+It is necessary that `μ` is absolutely continuous w.r.t. to Lebesgue measure and that `S` vary
+smoothly.  -/
+noncomputable
+def _root_.MeasureTheory.Measure.restrictToFrontier (μ : Measure X) (S : W → Set X) (w dw : W) :
+    VectorMeasure X R where
+  measureOf' := fun A =>
+    let s := fun x => (frontierSpeed R S w dw x)
+    let dμdV := fun x => (μ.rnDeriv volume x).toReal
+    ∫ x in A ∩ S w, s x * dμdV x ∂(surfaceMeasure (finrank R X - 1))
+  empty' := sorry_proof
+  not_measurable' := sorry_proof
+  m_iUnion' := sorry_proof
+
+
+variable {R}
+
+
+/-- Restrict measure `μ` to `θ` level set of a function `φ` obtaining (n-1)-dimensional integral -/
+noncomputable
+def _root_.MeasureTheory.Measure.restrictToLevelSet (μ : Measure X) (φ : W → X → R) (w dw : W) :
+    VectorMeasure X R := μ.restrictToFrontier R (fun w => {x | φ w x ≤ 0}) w dw
+
+
+@[ftrans_simp]
+theorem restrictToFrontier_eq_restrictToLevelSet (μ : Measure X) (φ ψ : W → X → R) :
+  μ.restrictToFrontier R (fun w => {x | φ w x ≤ ψ w x})
+  =
+  μ.restrictToLevelSet (fun w x => φ w x - ψ w x) := sorry_proof
+
+
+-- /-- Volume integral can be split into integral over reals and level sets.
+
+--   TODO: add proper assumptions:
+--             - integrability of f
+--             - non-zero gradient of `φ` almost everywhere
+--             - `μ ≪ volume`
+-- -/
+-- theorem cintegral_cintegral_conditionOn (f : X → U) (φ : X → R) (μ : Measure X) :
+--     ∫' t, ∫' x, f x ∂(μ.restrictToLevelSet (fun t x => φ x - t) t)
+--     =
+--     ∫' x, f x ∂μ := sorry_proof
+
+
+
+-- /-- Derivative of integral over sub-levelsets is equal to the integral over level set.
+
+--   TODO: add proper assumptions:
+--             - integrability of f
+--             - non-zero gradient of `φ` almost everywhere
+--             - `μ ≪ volume`
+-- -/
+-- theorem cderiv_cintegral_in_level_set (f : X → U) (φ : W → X → R) (μ : Measure X) :
+--     (cderiv R fun w => ∫' x in {x | φ w x ≤ 0}, f x ∂μ)
+--     =
+--     fun w dw => dw • ∫' x, f x ∂(μ.restrictToLevelSet φ w dw) := sorry_proof

SciLean/Core/Integral/RnDeriv.lean

@@ -0,0 +1,36 @@
+import Mathlib.MeasureTheory.Decomposition.Lebesgue
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
+
+import SciLean.Tactic.FTrans.Simp
+
+namespace SciLean
+
+open MeasureTheory
+
+/-! WARNING: This file contains rewrite rules for Radon-Nikodym derivative which usually hold
+  almost everywhere but here we postulate them as equalities everywhere. This is because we are
+  lacking proper automation to apply equalities that hold only almost everywhere.
+ -/
+
+
+open Classical in
+@[ftrans_simp]
+theorem rnDeriv_restrict {X} [MeasurableSpace X] (μ ν : Measure X) (A : Set X) :
+  (μ.restrict A).rnDeriv ν
+  =
+  fun x => (μ.rnDeriv ν x) * (if x ∈ A then 1 else 0) := sorry_proof
+
+
+@[ftrans_simp]
+theorem rnDeriv_prod_volume {X Y} [MeasureSpace X] [MeasureSpace Y] (μ : Measure X) (ν : Measure Y) :
+  (μ.prod ν).rnDeriv volume
+  =
+  fun (x,y) => (μ.rnDeriv volume x) * (ν.rnDeriv volume y) := sorry_proof
+
+
+-- This is pointwise version of: MeasureTheorey.Measure.rnDeriv_self
+@[ftrans_simp]
+theorem rnDeriv_self {X} [MeasurableSpace X] (μ : Measure X) :
+  μ.rnDeriv μ
+  =
+  fun _ => 1 := sorry_proof

SciLean/Core/Integral/Surface.lean

@@ -35,3 +35,8 @@ open FiniteDimensional in
 @[simp, ftrans_simp]
 theorem surfaceMeasure_volume [MeasureSpace X] :
    surfaceMeasure (X:=X) (finrank R X) = volume := sorry_proof
+
+
+@[ftrans_simp]
+theorem surfaceMeasure_zero_singleton [MeasureSpace X] (x : X) :
+  surfaceMeasure 0 {x} = 1 := sorry_proof