Coarse-graining support: Support.Sobolev.W1p.ConvexApproxSmoothing.Continuity

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Continuity, pointwise fderiv, and ae-equality for the smoothing

Concludes the weak-derivative chain with ae_eq_fderiv_convexApproxSmoothRepresentative_apply_basisVec, then pivots to the pointwise-classical world: continuity of convexApproxSample, convexApproxIntegrand, and the derived oscillation / weighted / kernel-times- const integrands; continuity of convexApproxSmoothing; the parametric convexApproxFDerivIntegrand and the explicit hasFDerivAt_convexApproxSmoothing_of_contDiff computation (including its apply_basisVec form).

theorem HCPolySupport.ae_eq_fderiv_convexApproxSmoothRepresentative_apply_basisVec {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {i : Fin d} {u gi ρ : Vec d → ℝ} {p : ENNReal} (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (huMem : MemLpOn U p u) (hgiMem : MemLpOn U p gi) (huWeak : HasWeakPartialDerivOn U i u gi) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : (fun (x : Vec d) => (fderiv ℝ (convexApproxSmoothRepresentative U ρ u x0 r ε) x) (basisVec i)) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => (1 - ε) * convexApproxSmoothRepresentative U ρ gi x0 r ε x

theorem HCPolySupport.continuous_convexApproxSample_right {d : ℕ} (x0 : Vec d) (r ε : ℝ) (x : Vec d) : Continuous fun (z : Vec d) => convexApproxSample x0 z r ε x

theorem HCPolySupport.continuous_convexApproxSample_prod {d : ℕ} (x0 : Vec d) (r ε : ℝ) : Continuous fun (p : Vec d × Vec d) => convexApproxSample x0 p.2 r ε p.1

theorem HCPolySupport.continuous_convexApproxIntegrand_right {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : Continuous fun (z : Vec d) => convexApproxIntegrand ρ u x0 r ε x z

theorem HCPolySupport.continuous_convexApproxIntegrand_left {d : ℕ} {ρ u : Vec d → ℝ} (hu : Continuous u) (x0 z : Vec d) (r ε : ℝ) : Continuous fun (x : Vec d) => convexApproxIntegrand ρ u x0 r ε x z

theorem HCPolySupport.continuous_convexApproxIntegrand_prod {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) : Continuous fun (p : Vec d × Vec d) => convexApproxIntegrand ρ u x0 r ε p.1 p.2

theorem HCPolySupport.tsupport_convexApproxIntegrand_subset {d : ℕ} {ρ u : Vec d → ℝ} (x0 : Vec d) (r ε : ℝ) (x : Vec d) : (tsupport fun (z : Vec d) => convexApproxIntegrand ρ u x0 r ε x z) ⊆ tsupport ρ

theorem HCPolySupport.hasCompactSupport_convexApproxIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ : HasCompactSupport ρ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : HasCompactSupport fun (z : Vec d) => convexApproxIntegrand ρ u x0 r ε x z

theorem HCPolySupport.integrable_convexApproxIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : MeasureTheory.Integrable (fun (z : Vec d) => convexApproxIntegrand ρ u x0 r ε x z) MeasureTheory.volume

theorem HCPolySupport.continuous_convexApproxDifferenceIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : Continuous fun (z : Vec d) => ρ z * (u (convexApproxSample x0 z r ε x) - u x)

theorem HCPolySupport.hasCompactSupport_convexApproxDifferenceIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ_compact : HasCompactSupport ρ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : HasCompactSupport fun (z : Vec d) => ρ z * (u (convexApproxSample x0 z r ε x) - u x)

theorem HCPolySupport.integrable_convexApproxDifferenceIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : MeasureTheory.Integrable (fun (z : Vec d) => ρ z * (u (convexApproxSample x0 z r ε x) - u x)) MeasureTheory.volume

theorem HCPolySupport.continuous_convexApproxWeightedOscillation {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : Continuous fun (z : Vec d) => ρ z * |u (convexApproxSample x0 z r ε x) - u x|

theorem HCPolySupport.hasCompactSupport_convexApproxWeightedOscillation {d : ℕ} {ρ u : Vec d → ℝ} (hρ_compact : HasCompactSupport ρ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : HasCompactSupport fun (z : Vec d) => ρ z * |u (convexApproxSample x0 z r ε x) - u x|

theorem HCPolySupport.integrable_convexApproxWeightedOscillation {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : MeasureTheory.Integrable (fun (z : Vec d) => ρ z * |u (convexApproxSample x0 z r ε x) - u x|) MeasureTheory.volume

theorem HCPolySupport.integrable_convexApproxKernelMulConst {d : ℕ} {ρ : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (c : ℝ) : MeasureTheory.Integrable (fun (z : Vec d) => ρ z * c) MeasureTheory.volume

theorem HCPolySupport.continuous_convexApproxSmoothing {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) : Continuous (convexApproxSmoothing ρ u x0 r ε)

noncomputable def HCPolySupport.convexApproxFDerivIntegrand {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x z : Vec d) : Vec d →L[ℝ] ℝ

The pointwise Fréchet-derivative integrand of the convex smoothing operator.

Equations

• HCPolySupport.convexApproxFDerivIntegrand ρ u x0 r ε x z = (ρ z * (1 - ε)) • fderiv ℝ u (HCPolySupport.convexApproxSample x0 z r ε x)

@[simp]

theorem HCPolySupport.convexApproxFDerivIntegrand_apply {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x z : Vec d) : convexApproxFDerivIntegrand ρ u x0 r ε x z = (ρ z * (1 - ε)) • fderiv ℝ u (convexApproxSample x0 z r ε x)

theorem HCPolySupport.continuous_convexApproxFDerivIntegrand_right {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : Continuous fun (z : Vec d) => convexApproxFDerivIntegrand ρ u x0 r ε x z

theorem HCPolySupport.hasCompactSupport_convexApproxFDerivIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ_compact : HasCompactSupport ρ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : HasCompactSupport fun (z : Vec d) => convexApproxFDerivIntegrand ρ u x0 r ε x z

theorem HCPolySupport.integrable_convexApproxFDerivIntegrand {d : ℕ} {ρ u : Vec d → ℝ} (hρ : Continuous ρ) (hρ_compact : HasCompactSupport ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : MeasureTheory.Integrable (fun (z : Vec d) => convexApproxFDerivIntegrand ρ u x0 r ε x z) MeasureTheory.volume

theorem HCPolySupport.hasFDerivAt_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : HasFDerivAt (convexApproxSample x0 z r ε) ((1 - ε) • ContinuousLinearMap.id ℝ (Vec d)) x

theorem HCPolySupport.hasFDerivAt_convexApproxIntegrand_left_of_contDiff {d : ℕ} {ρ u : Vec d → ℝ} (_hρ : Continuous ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x z : Vec d) : HasFDerivAt (fun (y : Vec d) => convexApproxIntegrand ρ u x0 r ε y z) (convexApproxFDerivIntegrand ρ u x0 r ε x z) x

theorem HCPolySupport.hasFDerivAt_convexApproxSmoothing_of_contDiff {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : HasFDerivAt (convexApproxSmoothing ρ u x0 r ε) (∫ (z : Vec d) in tsupport ρ, convexApproxFDerivIntegrand ρ u x0 r ε x z) x

theorem HCPolySupport.fderiv_convexApproxSmoothing_of_contDiff {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : fderiv ℝ (convexApproxSmoothing ρ u x0 r ε) x = ∫ (z : Vec d) in tsupport ρ, convexApproxFDerivIntegrand ρ u x0 r ε x z

theorem HCPolySupport.fderiv_convexApproxSmoothing_apply_basisVec_of_contDiff {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : ContDiff ℝ 1 u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) (i : Fin d) : (fderiv ℝ (convexApproxSmoothing ρ u x0 r ε) x) (basisVec i) = (1 - ε) * convexApproxSmoothing ρ (fun (y : Vec d) => (fderiv ℝ u y) (basisVec i)) x0 r ε x