ApproximationAssembly

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

Provider: part (i) of l.approximation.stationary.by.local on the potential subspace

The three inputs are

• the cutoff estimates of Algsuperdiff/Section3/Provider/Corrector/PotentialApproximation.lean, run against the mollified field q = mollifyGrad ρ φ;
• a pointwise Young split ‖a + b‖² ≤ (1 + δ)‖a‖² + (1 + δ⁻¹)‖b‖² together with the stationary transfer E[⨍_{cu_K}|realize (q − p)|²] = E[|q − p|²] (integral_setIntegral_normSq_realize), which converts the estimate for q into one for p; and
• the density of the mollified gradients (exists_mollifyGrad_integral_normSq_sub_le), which makes ‖q − p‖_{L²(Ω)} as small as one wishes.

No sublinearity and no ergodic-theoretic input is used.

Elementary Young inequalities

theorem Algsuperdiff.Section3.Provider.Corrector.two_mul_le_young {δ x y : ℝ} (hδ : 0 < δ) : 2 * (x * y) ≤ δ * x ^ 2 + δ⁻¹ * y ^ 2

The scalar Young inequality 2xy ≤ δx² + δ⁻¹y².

theorem Algsuperdiff.Section3.Provider.Corrector.normSq_add_le_young {E : Type u_1} [NormedAddCommGroup E] {δ : ℝ} (hδ : 0 < δ) (a b : E) : ‖a + b‖ ^ 2 ≤ (1 + δ) * ‖a‖ ^ 2 + (1 + δ⁻¹) * ‖b‖ ^ 2

The vector Young inequality ‖a + b‖² ≤ (1 + δ)‖a‖² + (1 + δ⁻¹)‖b‖².

theorem Algsuperdiff.Section3.Provider.Corrector.young_density_arith {M P s δ η D A e : ℝ} (hM0 : 0 ≤ M) (hMD : M ≤ D) (hP0 : 0 ≤ P) (hs0 : 0 < s) (hs1 : s ≤ 1) (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) (hsbound : s * (D * (2 * P + 1) + 1) ≤ η / 3) (hδbound : δ * (D * (P + 1) ^ 2 + 1) ≤ η / 3) (hsδ : s ≤ δ * η / 6) (hA : A ≤ (P + s) ^ 2) (he : e ≤ s ^ 2) : (1 + δ) * (M * A) + (1 + δ⁻¹) * e ≤ M * P ^ 2 + η

The algebraic core of the density step: with δ and s chosen small the Young split of a nearby field costs less than η.

The local approximant against a different target field

theorem Algsuperdiff.Section3.Provider.Corrector.realize_sub_apply {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] (q p : Ω → HCPolySupport.HilbertVec d) (ω : Ω) (x : HCPolySupport.Vec d) : realize (fun (ω' : Ω) => q ω' - p ω') ω x = realize q ω x - realize p ω x

The realization of a difference is the difference of the realizations.

theorem Algsuperdiff.Section3.Provider.Corrector.localGradApprox_sub_realize_split {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] (Q : HCPolySupport.TriadicCube d) (L : ℕ) (φ : Ω → ℝ) (q p : Ω → HCPolySupport.HilbertVec d) (ω : Ω) (x : HCPolySupport.Vec d) : HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize p ω x = HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize q ω x + realize (fun (ω' : Ω) => q ω' - p ω') ω x

The error against a target field p splits into the error against the mollified field q and the stationary remainder q - p.

theorem Algsuperdiff.Section3.Provider.Corrector.norm_localGradApprox_sub_realize_le {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] (Q : HCPolySupport.TriadicCube d) (L : ℕ) (φ : Ω → ℝ) (q : Ω → HCPolySupport.HilbertVec d) (ω : Ω) (x : HCPolySupport.Vec d) : ‖HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize q ω x‖ ≤ ‖realize q ω x‖ + gradBound Q L * ‖realize φ ω x‖

A crude pointwise bound on the local approximation error, valid at every point of space.

The cube estimate against a different target field

theorem Algsuperdiff.Section3.Provider.Corrector.ae_memLp_localGradApprox_sub {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) (L : ℕ) {φ : Ω → ℝ} {q : Ω → HCPolySupport.HilbertVec d} (hφm : MeasureTheory.StronglyMeasurable φ) (hφ : MeasureTheory.MemLp φ 2 μ) (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 μ) : ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize q ω x) 2 (MeasureTheory.volume.restrict (HCPolySupport.cubeSet Q))

For almost every sample the local approximation error is square integrable on the cube.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_setIntegral_normSq_localGradApprox_sub {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) (L : ℕ) {φ : Ω → ℝ} {q : Ω → HCPolySupport.HilbertVec d} (hφm : MeasureTheory.StronglyMeasurable φ) (hφ : MeasureTheory.MemLp φ 2 μ) (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 μ) : MeasureTheory.Integrable (fun (ω : Ω) => ∫ (x : HCPolySupport.Vec d) in HCPolySupport.cubeSet Q, ‖HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize q ω x‖ ^ 2) μ

The set integral of the squared local approximation error is integrable in the sample.

theorem Algsuperdiff.Section3.Provider.Corrector.integral_setIntegral_normSq_localGradApprox_sub_target_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) (L : ℕ) {δ : ℝ} (hδ : 0 < δ) {φ : Ω → ℝ} {q p : Ω → HCPolySupport.HilbertVec d} (hφm : MeasureTheory.StronglyMeasurable φ) (hφ : MeasureTheory.MemLp φ 2 μ) (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 μ) (hpm : MeasureTheory.StronglyMeasurable p) (hp : MeasureTheory.MemLp p 2 μ) : ∫ (ω : Ω), ∫ (x : HCPolySupport.Vec d) in HCPolySupport.cubeSet Q, ‖HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize p ω x‖ ^ 2 ∂μ ≤ (1 + δ) * ∫ (ω : Ω), ∫ (x : HCPolySupport.Vec d) in HCPolySupport.cubeSet Q, ‖HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize q ω x‖ ^ 2 ∂μ + (1 + δ⁻¹) * (HCPolySupport.cubeVolume Q * ∫ (ω : Ω), ‖q ω - p ω‖ ^ 2 ∂μ)

The Young transfer at a fixed cube. The expected squared error of the local approximant against an arbitrary target field p is controlled by its error against the mollified field q plus the stationary distance from q to p.

theorem Algsuperdiff.Section3.Provider.Corrector.integral_cubeLpNorm_localGradApprox_sub_target_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) (L : ℕ) {δ : ℝ} (hδ : 0 < δ) {φ : Ω → ℝ} {q p : Ω → HCPolySupport.HilbertVec d} (hφm : MeasureTheory.StronglyMeasurable φ) (hφ : MeasureTheory.MemLp φ 2 μ) (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 μ) (hpm : MeasureTheory.StronglyMeasurable p) (hp : MeasureTheory.MemLp p 2 μ) : ∫ (ω : Ω), (HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize p ω x) ^ 2 ∂μ ≤ (1 + δ) * (↑d * 3 ^ (-↑L) * ∫ (ω : Ω), ‖q ω‖ ^ 2 ∂μ + 2 * gradBound Q L ^ 2 * ∫ (ω : Ω), ‖φ ω‖ ^ 2 ∂μ) + (1 + δ⁻¹) * ∫ (ω : Ω), ‖q ω - p ω‖ ^ 2 ∂μ

The L²(Q)-normalized form of the Young transfer.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_cubeLpNorm_localGradApprox_sub_target {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) (L : ℕ) {φ : Ω → ℝ} {q p : Ω → HCPolySupport.HilbertVec d} (hφm : MeasureTheory.StronglyMeasurable φ) (hφ : MeasureTheory.MemLp φ 2 μ) (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 μ) (hpm : MeasureTheory.StronglyMeasurable p) (hp : MeasureTheory.MemLp p 2 μ) : MeasureTheory.Integrable (fun (ω : Ω) => (HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (localGradApprox Q L φ q ω x) - realize p ω x) ^ 2) μ

The squared normalized error against the target p is integrable in the sample — the integrand of the part-(i) display.

Part (i) on the stationary potential subspace

theorem Algsuperdiff.Section3.Provider.Corrector.exists_family_bound {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] [TopologicalSpace Ω] [R1Space Ω] [BorelSpace Ω] [ContinuousVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] (L : ℕ) {η : ℝ} (hη : 0 < η) {p : Ω → HCPolySupport.HilbertVec d} (hpm : MeasureTheory.StronglyMeasurable p) (hp : MeasureTheory.MemLp p 2 μ) (hmem : MeasureTheory.MemLp.toLp p hp ∈ Probability.Stationary.stationaryPotentialSubspace) : ∃ (V : ℕ → Ω → HCPolySupport.Vec d → HCPolySupport.Vec d) (g : ℕ → ℝ), (∀ (K : ℕ), 0 ≤ g K) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ (∀ (K : ℕ), ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.IsPotentialZeroTraceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (V K ω)) ∧ (∀ (K : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => (HCPolySupport.cubeLpNorm (HCPolySupport.originCube d ↑K) 2 fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (V K ω x) - realize p ω x) ^ 2) μ) ∧ ∀ (K : ℕ), ∫ (ω : Ω), (HCPolySupport.cubeLpNorm (HCPolySupport.originCube d ↑K) 2 fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (V K ω x) - realize p ω x) ^ 2 ∂μ ≤ ↑d * 3 ^ (-↑L) * ∫ (ω : Ω), ‖p ω‖ ^ 2 ∂μ + η + g K

The approximation family at a prescribed tolerance. For every η > 0 there is a family of zero-trace potentials on the origin cubes whose expected normalized error against p exceeds the target d·3^{-L}·E[|p|²] by at most η plus a term that vanishes as the cube grows.