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

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

Convex-domain smoothing kernel

Defines the Riesz-style smoothing kernel IsConvexApproxKernel, produces a concrete unit kernel from a ContDiffBump, and assembles the convexApproxSmoothing operator. The scaled kernel's analytic properties (continuity, smoothness, measurability, compact support, integrability, nonnegativity, unit integral) together with the convolution rewrite of the smoothing operator live here; everything downstream builds on this file.

structure HCPolySupport.IsConvexApproxKernel {d : ℕ} (ρ : Vec d → ℝ) : Prop

The kernel is smooth and nonnegative, has compact topological support in the closed unit ball, and has integral one over its support.

• smooth : ContDiff ℝ (↑⊤) ρ
• compactSupport : HasCompactSupport ρ
• support_subset_closedBall : tsupport ρ ⊆ Metric.closedBall 0 1
• nonneg (z : Vec d) : 0 ≤ ρ z
• setIntegral_one : ∫ (z : Vec d) in tsupport ρ, ρ z = 1

theorem HCPolySupport.IsConvexApproxKernel.continuous {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) : Continuous ρ

theorem HCPolySupport.ContDiffBump.isConvexApproxKernel_normed {d : ℕ} (φ : ContDiffBump 0) (hφ : φ.rOut ≤ 1) : IsConvexApproxKernel (φ.normed MeasureTheory.volume)

noncomputable def HCPolySupport.unitContDiffBump {d : ℕ} : ContDiffBump 0

A concrete bump centered at the origin with outer radius 1.

Equations

• HCPolySupport.unitContDiffBump = { rIn := 1 / 2, rOut := 1, rIn_pos := HCPolySupport.unitContDiffBump._proof_1, rIn_lt_rOut := HCPolySupport.unitContDiffBump._proof_2 }

noncomputable def HCPolySupport.unitConvexApproxKernel {d : ℕ} : Vec d → ℝ

The corresponding normalized smooth kernel supported in closedBall 0 1.

Equations

• HCPolySupport.unitConvexApproxKernel = HCPolySupport.unitContDiffBump.normed MeasureTheory.volume

theorem HCPolySupport.isConvexApproxKernel_unitConvexApproxKernel {d : ℕ} : IsConvexApproxKernel unitConvexApproxKernel

noncomputable def HCPolySupport.unitConvexApproxScale (n : ℕ) : ℝ

The standard scale sequence used for the concrete approximation family.

Equations

• HCPolySupport.unitConvexApproxScale n = 1 / (↑n + 1)

theorem HCPolySupport.unitConvexApproxScale_nonneg (n : ℕ) : 0 ≤ unitConvexApproxScale n

theorem HCPolySupport.unitConvexApproxScale_le_one (n : ℕ) : unitConvexApproxScale n ≤ 1

theorem HCPolySupport.tendsto_unitConvexApproxScale_zero : Filter.Tendsto unitConvexApproxScale Filter.atTop (nhds 0)

def HCPolySupport.convexApproxIntegrand {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x z : Vec d) : ℝ

The pointwise integrand for the convex-domain smoothing operator.

Equations

• HCPolySupport.convexApproxIntegrand ρ u x0 r ε x z = ρ z * u (HCPolySupport.convexApproxSample x0 z r ε x)

@[simp]

theorem HCPolySupport.convexApproxIntegrand_apply {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x z : Vec d) : convexApproxIntegrand ρ u x0 r ε x z = ρ z * u (convexApproxSample x0 z r ε x)

noncomputable def HCPolySupport.convexApproxSmoothing {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : ℝ

The convex-domain smoothing operator attached to a kernel ρ.

Equations

• HCPolySupport.convexApproxSmoothing ρ u x0 r ε x = ∫ (z : HCPolySupport.Vec d) in tsupport ρ, HCPolySupport.convexApproxIntegrand ρ u x0 r ε x z

@[simp]

theorem HCPolySupport.convexApproxSmoothing_apply {d : ℕ} (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : convexApproxSmoothing ρ u x0 r ε x = ∫ (z : Vec d) in tsupport ρ, convexApproxIntegrand ρ u x0 r ε x z

noncomputable def HCPolySupport.unitConvexApproxSequence {d : ℕ} (u : Vec d → ℝ) (x0 : Vec d) (r : ℝ) (n : ℕ) : Vec d → ℝ

The concrete convex smoothing sequence built from the unit normalized kernel.

Equations

• HCPolySupport.unitConvexApproxSequence u x0 r n x = HCPolySupport.convexApproxSmoothing HCPolySupport.unitConvexApproxKernel u x0 r (HCPolySupport.unitConvexApproxScale n) x

noncomputable def HCPolySupport.scaledConvexApproxKernel {d : ℕ} (ρ : Vec d → ℝ) (a : ℝ) : Vec d → ℝ

The Euclidean rescaling of a kernel by a positive factor a.

Equations

• HCPolySupport.scaledConvexApproxKernel ρ a y = (a ^ d)⁻¹ * ρ (a⁻¹ • y)

theorem HCPolySupport.continuous_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : Continuous ρ) (a : ℝ) : Continuous (scaledConvexApproxKernel ρ a)

theorem HCPolySupport.contDiff_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (a : ℝ) : ContDiff ℝ (↑⊤) (scaledConvexApproxKernel ρ a)

theorem HCPolySupport.measurable_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : Continuous ρ) (a : ℝ) : Measurable (scaledConvexApproxKernel ρ a)

theorem HCPolySupport.hasCompactSupport_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : HasCompactSupport ρ) {a : ℝ} (ha : 0 < a) : HasCompactSupport (scaledConvexApproxKernel ρ a)

theorem HCPolySupport.integrable_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {a : ℝ} (ha : 0 < a) : MeasureTheory.Integrable (scaledConvexApproxKernel ρ a) MeasureTheory.volume

theorem HCPolySupport.scaledConvexApproxKernel_nonneg {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {a : ℝ} (ha : 0 < a) (y : Vec d) : 0 ≤ scaledConvexApproxKernel ρ a y

theorem HCPolySupport.integral_scaledConvexApproxKernel {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {a : ℝ} (ha : 0 < a) : ∫ (y : Vec d), scaledConvexApproxKernel ρ a y = 1

theorem HCPolySupport.convexApproxImage_subset_translateSet_smul {d : ℕ} {U : Set (Vec d)} (x0 z : Vec d) (r ε : ℝ) : convexApproxSample x0 z r ε '' U ⊆ translateSet (ε • (x0 - r • z)) ((1 - ε) • U)

theorem HCPolySupport.translateSet_smul_subset_of_convexApproxSample_mapsTo {d : ℕ} {U : Set (Vec d)} {x0 z : Vec d} {r ε : ℝ} (hmap : Set.MapsTo (convexApproxSample x0 z r ε) U U) : translateSet (ε • (x0 - r • z)) ((1 - ε) • U) ⊆ U

theorem HCPolySupport.setIntegral_comp_smul_add_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) (b : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (x : Vec d) in U, f (a • x + b) = (a ^ d)⁻¹ • ∫ (y : Vec d) in translateSet b (a • U), f y

theorem HCPolySupport.setIntegral_comp_inv_smul_sub_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) (b : Vec d) (U : Set (Vec d)) (f : Vec d → E) : (a ^ d)⁻¹ • ∫ (y : Vec d) in translateSet b (a • U), f (a⁻¹ • (y - b)) = ∫ (x : Vec d) in U, f x

theorem HCPolySupport.convolution_scaledConvexApproxKernel_indicator_eq_setIntegral {d : ℕ} {ρ u : Vec d → ℝ} {U : Set (Vec d)} {x0 x : Vec d} {r ε : ℝ} (hr : 0 < r) (hε0 : 0 < ε) : MeasureTheory.convolution (scaledConvexApproxKernel ρ (ε * r)) (U.indicator u) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume ((1 - ε) • x + ε • x0) = ∫ (z : Vec d) in tsupport ρ, ρ z * U.indicator u ((1 - ε) • x + ε • x0 - (ε * r) • z)

theorem HCPolySupport.convexApproxSmoothing_eq_convolution_scaledConvexApproxKernel_indicator {d : ℕ} {ρ u : Vec d → ℝ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) {x0 x : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : convexApproxSmoothing ρ u x0 r ε x = MeasureTheory.convolution (scaledConvexApproxKernel ρ (ε * r)) (U.indicator u) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume ((1 - ε) • x + ε • x0)