Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.W1p.ConvexApproxSmoothing.Convergence

Coarse-graining support: Support.Sobolev.W1p.ConvexApproxSmoothing.Convergence #

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

L^p convergence of the convex smoothing #

The tendsto theorems: pointwise convergence of the partial fderivs on contDiff data; the matching eLpNorm tendstos for fderiv, for the pure convexApproxSmoothing u − u difference at continuous data, then upgraded to MemLpOn; and their one_sub_mul cutoff-weighted variants. The corresponding statements for unitConvexApproxSequence close the file.

source
theorem HCPolySupport.eventually_forall_abs_fderiv_convexApproxSmoothing_apply_basisVec_sub_le_of_contDiff {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hu : ContDiff ℝ 1 u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ε n) (hε_le_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n ≤ 1) (i : Fin d) {δ : ℝ} (hδ : 0 < δ) :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ ⦃x : Vec d⦄, x ∈ U → |(fderiv ℝ (convexApproxSmoothing ρ u x0 r (ε n)) x) (basisVec i) - (fderiv ℝ u x) (basisVec i)| ≤ δ
source
theorem HCPolySupport.eventually_forall_abs_fderiv_unitConvexApproxSequence_apply_basisVec_sub_le_of_contDiff {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hu : ContDiff ℝ 1 u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (i : Fin d) {δ : ℝ} (hδ : 0 < δ) :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ ⦃x : Vec d⦄, x ∈ U → |(fderiv ℝ (unitConvexApproxSequence u x0 r n) x) (basisVec i) - (fderiv ℝ u x) (basisVec i)| ≤ δ
source
theorem HCPolySupport.tendsto_fderiv_unitConvexApproxSequence_apply_basisVec_of_contDiff {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hu : ContDiff ℝ 1 u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (i : Fin d) {x : Vec d} (hx : x ∈ U) :
Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (unitConvexApproxSequence u x0 r n) x) (basisVec i)) Filter.atTop (nhds ((fderiv ℝ u x) (basisVec i)))
source
theorem HCPolySupport.tendsto_eLpNorm_fderiv_convexApproxSmoothing_apply_basisVec_sub_zero_of_contDiff {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp : p ≠ ⊤) (hu : ContDiff ℝ 1 u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ε n) (hε_le_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n ≤ 1) (i : Fin d) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (convexApproxSmoothing ρ u x0 r (ε n)) x) (basisVec i) - (fderiv ℝ u x) (basisVec i)) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_fderiv_unitConvexApproxSequence_apply_basisVec_sub_zero_of_contDiff {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp : p ≠ ⊤) (hu : ContDiff ℝ 1 u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (i : Fin d) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (unitConvexApproxSequence u x0 r n) x) (basisVec i) - (fderiv ℝ u x) (basisVec i)) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_convexApproxSmoothing_of_continuous {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp : p ≠ ⊤) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ε n) (hε_le_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n ≤ 1) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => convexApproxSmoothing ρ u x0 r (ε n) x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_unitConvexApproxSequence_of_continuous {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp : p ≠ ⊤) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => unitConvexApproxSequence u x0 r n x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_convexApproxSmoothing_of_memLpOn {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ε n) (hε_lt_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n < 1) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => convexApproxSmoothing ρ u x0 r (ε n) x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_one_sub_mul_convexApproxSmoothing_of_memLpOn {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ε n) (hε_lt_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n < 1) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (1 - ε n) * convexApproxSmoothing ρ u x0 r (ε n) x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_unitConvexApproxSequence_of_memLpOn {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => unitConvexApproxSequence u x0 r n x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
source
theorem HCPolySupport.tendsto_eLpNorm_sub_zero_one_sub_mul_unitConvexApproxSequence_of_memLpOn {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (1 - unitConvexApproxScale n) * unitConvexApproxSequence u x0 r n x - u x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)