KernelIdentificationOpenApprox

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Compactly supported approximation of open-set indicators

This module constructs an increasing sequence of compactly supported continuous functions converging pointwise to the indicator of a proper open set.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.rawOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : ℝ

A compactly supported continuous distance cutoff for an open set.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.rawOpenApprox G n x = min 1 ((↑n + 1) * Metric.infDist x Gᶜ) * DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeBoundaryCutoff n x

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : ℝ

The bounded cumulative sum of open-set distance cutoffs.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpaceOpenApprox G n x = min 1 (∑ k ∈ Finset.range (n + 1), DivergenceFormProcess.Form.WholeSpaceAnalyticData.rawOpenApprox G k x)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuous_wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) : Continuous (wholeSpaceOpenApprox G n)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasCompactSupport_wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) : HasCompactSupport (wholeSpaceOpenApprox G n)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpaceOpenApproxC0 {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ

The cumulative open-set cutoff bundled as a function vanishing at infinity.

Equations

• One or more equations did not get rendered due to their size.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpaceOpenApprox_nonneg {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : 0 ≤ wholeSpaceOpenApprox G n x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.monotone_wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (x : HCPolySupport.Vec d) : Monotone fun (n : ℕ) => wholeSpaceOpenApprox G n x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.iSup_wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (hG : IsOpen G) (hGne : G ≠ Set.univ) (x : HCPolySupport.Vec d) : ⨆ (n : ℕ), ENNReal.ofReal (wholeSpaceOpenApprox G n x) = G.indicator (fun (x : HCPolySupport.Vec d) => 1) x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_wholeSpaceOpenApprox {d : ℕ} (G : Set (HCPolySupport.Vec d)) (hG : IsOpen G) (hGne : G ≠ Set.univ) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (n : ℕ) => wholeSpaceOpenApprox G n x) Filter.atTop (nhds (G.indicator (fun (x : HCPolySupport.Vec d) => 1) x))

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_wholeSpaceOpenApprox_le_one {d : ℕ} (G : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : |wholeSpaceOpenApprox G n x| ≤ 1