Approx

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

The C¹ chain rule for H¹ via mollification

hasWeakGradientOn_comp_of_deriv_bounded: for u ∈ H¹(U) and G of class C¹ with |G'| ≤ M, the composite G ∘ u has weak gradient G'(u) · ∇u.

One-sided smooth approximators G_δ → (·−c)₊

noncomputable def HCPolySupport.gStep (c δ t : ℝ) : ℝ

Smooth step: 0 for t ≤ c+δ, 1 for t ≥ c+2δ, in [0,1].

Equations

• HCPolySupport.gStep c δ t = ((t - c) / δ - 1).smoothTransition

noncomputable def HCPolySupport.GApprox (c δ t : ℝ) : ℝ

One-sided smooth approximant to (·−c)₊, an antiderivative of gStep.

Equations

• HCPolySupport.GApprox c δ t = ∫ (s : ℝ) in c..t, HCPolySupport.gStep c δ s

theorem HCPolySupport.gStep_contDiff (c δ : ℝ) : ContDiff ℝ (↑⊤) (gStep c δ)

theorem HCPolySupport.gStep_continuous (c δ : ℝ) : Continuous (gStep c δ)

theorem HCPolySupport.gStep_nonneg (c δ t : ℝ) : 0 ≤ gStep c δ t

theorem HCPolySupport.gStep_le_one (c δ t : ℝ) : gStep c δ t ≤ 1

theorem HCPolySupport.gStep_eq_zero {c δ t : ℝ} (hδ : 0 < δ) (ht : t ≤ c + δ) : gStep c δ t = 0

theorem HCPolySupport.gStep_eq_one {c δ t : ℝ} (hδ : 0 < δ) (ht : c + 2 * δ ≤ t) : gStep c δ t = 1

theorem HCPolySupport.gStep_intervalIntegrable (c δ a b : ℝ) : IntervalIntegrable (gStep c δ) MeasureTheory.volume a b

theorem HCPolySupport.GApprox_hasDerivAt (c δ t : ℝ) : HasDerivAt (GApprox c δ) (gStep c δ t) t

theorem HCPolySupport.deriv_GApprox (c δ : ℝ) : deriv (GApprox c δ) = gStep c δ

theorem HCPolySupport.GApprox_contDiff_one (c δ : ℝ) : ContDiff ℝ 1 (GApprox c δ)

theorem HCPolySupport.abs_deriv_GApprox_le (c δ t : ℝ) : |deriv (GApprox c δ) t| ≤ 1

theorem HCPolySupport.tendsto_gStep {c : ℝ} {δ : ℕ → ℝ} (hδpos : ∀ (n : ℕ), 0 < δ n) (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => gStep c (δ n) t) Filter.atTop (nhds (if c < t then 1 else 0))

The pointwise derivative limit: gStep c δₙ t → 𝟙_{t > c} for every t.

theorem HCPolySupport.abs_GApprox_le (c δ t : ℝ) : |GApprox c δ t| ≤ |t - c|

theorem HCPolySupport.abs_GApprox_sub_le {c δ : ℝ} (hδ : 0 < δ) (t : ℝ) : |GApprox c δ t - max (t - c) 0| ≤ 2 * δ

Uniform closeness of the approximant to the positive part.

theorem HCPolySupport.hasWeakGradientOn_comp_of_deriv_bounded {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {G : ℝ → ℝ} (hG : ContDiff ℝ 1 G) {M : ℝ} (hM : 0 ≤ M) (hderiv : ∀ (t : ℝ), |deriv G t| ≤ M) : HasWeakGradientOn U (fun (x : Vec d) => G (u.toFun x)) fun (x : Vec d) (i : Fin d) => deriv G (u.toFun x) * u.grad x i

C¹ chain rule (weak-gradient form).