ChainRule

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

C¹ chain-rule building blocks for H¹

Reusable sub-lemmas for the mollification chain rule: the pointwise fderiv chain-rule identity in coordinate form, the L² bound on a Lipschitz composition, and Lipschitz continuity from a derivative bound. These are the pieces the chain-rule argument threads together with the L² convergence of convexApproxSmoothing.

theorem HCPolySupport.lipschitzWith_of_abs_deriv_le {G : ℝ → ℝ} {M : ℝ} (hM : 0 ≤ M) (hG : Differentiable ℝ G) (hderiv : ∀ (t : ℝ), |deriv G t| ≤ M) : LipschitzWith M.toNNReal G

Lipschitz continuity of a real function from a bound on its derivative.

theorem HCPolySupport.fderiv_comp_basisVec {d : ℕ} {G : ℝ → ℝ} {w : Vec d → ℝ} {x : Vec d} {i : Fin d} (hG : DifferentiableAt ℝ G (w x)) (hw : DifferentiableAt ℝ w x) : (fderiv ℝ (fun (y : Vec d) => G (w y)) x) (basisVec i) = deriv G (w x) * (fderiv ℝ w x) (basisVec i)

Coordinate form of the chain rule: the i-th partial of G ∘ w is G'(w)·∂ᵢw.

theorem HCPolySupport.eLpNorm_comp_sub_le_of_lipschitz {d : ℕ} {U : Set (Vec d)} {G : ℝ → ℝ} {M : ℝ} (hM : 0 ≤ M) (hLip : LipschitzWith M.toNNReal G) (f g : Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (volumeMeasureOn U)) (hg : MeasureTheory.AEStronglyMeasurable g (volumeMeasureOn U)) : MeasureTheory.eLpNorm (fun (x : Vec d) => G (f x) - G (g x)) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal M * MeasureTheory.eLpNorm (fun (x : Vec d) => f x - g x) 2 (volumeMeasureOn U)

L² control of a Lipschitz composition: ‖G∘f − G∘g‖_{L²} ≤ M‖f − g‖_{L²}.