CutoffFieldLimitPointwise

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

Pointwise bounds survive the L² limit

A bound valid for every truncation a_L with L ≥ m is a bound on a family whose L² limit is the full-field solution. Two elementary transfers make it a bound on the limit.

From L² convergence to an almost-everywhere bound. If f_L ≤ c almost everywhere for all large L and ‖f_L - g‖_{L²} → 0, then g ≤ c almost everywhere: the positive part (g - c)_+ satisfies (g - c)_+ ≤ |f_L - g| almost everywhere, so its L² norm is at most ‖f_L - g‖_{L²} → 0, and a nonnegative function of vanishing L² norm vanishes almost everywhere.

From an almost-everywhere bound to a pointwise bound. On an open set, a function continuous there that satisfies a bound away from a null set satisfies it at every point. This is le_of_ae_le_of_continuousOn, applied against a constant.

Together: a bound holding for the continuous representatives of the truncated solutions, uniformly in L, holds at every point of the cube for the continuous representative of the full-field solution.

Main results

• ae_le_of_tendsto_l2, ae_ge_of_tendsto_l2 — the almost-everywhere transfer.
• le_on_open_subset_of_tendsto_l2, ge_on_open_subset_of_tendsto_l2 — the two combined, on an open subset of the cube, for continuous representatives.

References

• ABK26, the passage L → ∞ from the truncated fields a_L to a.

1. An L² limit inherits an almost-everywhere bound

theorem Algsuperdiff.Section5.Support.ae_le_of_tendsto_l2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) {f : ℤ → HCPolySupport.Vec d → ℝ} {g : HCPolySupport.Vec d → ℝ} {c : ℝ} (hf : ∀ (L : ℤ), MeasureTheory.MemLp (f L) 2 (MeasureTheory.volume.restrict U)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict U)) (hbound : ∀ᶠ (L : ℤ) in Filter.atTop, ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, f L x ≤ c) (hlim : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in U, (f L x - g x) ^ 2)) Filter.atTop (nhds 0)) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, g x ≤ c

An almost-everywhere upper bound passes to the L² limit.

theorem Algsuperdiff.Section5.Support.ae_ge_of_tendsto_l2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) {f : ℤ → HCPolySupport.Vec d → ℝ} {g : HCPolySupport.Vec d → ℝ} {c : ℝ} (hf : ∀ (L : ℤ), MeasureTheory.MemLp (f L) 2 (MeasureTheory.volume.restrict U)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict U)) (hbound : ∀ᶠ (L : ℤ) in Filter.atTop, ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, c ≤ f L x) (hlim : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in U, (f L x - g x) ^ 2)) Filter.atTop (nhds 0)) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, c ≤ g x

An almost-everywhere lower bound passes to the L² limit.

2. The transfer to the continuous representatives on the cube

theorem Algsuperdiff.Section5.Support.le_on_open_subset_of_tendsto_l2 {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {V : Set (HCPolySupport.Vec d)} (hVopen : IsOpen V) (hV : V ⊆ cubeSetAt y n) {u : ℤ → HCPolySupport.H1Function (cubeSetAt y n)} {uRep : ℤ → HCPolySupport.Vec d → ℝ} {v : HCPolySupport.H1Function (cubeSetAt y n)} {vRep : HCPolySupport.Vec d → ℝ} {c : ℝ} (hu : ∀ (L : ℤ), IsCubeRepresentative y n (u L) (uRep L)) (hv : IsCubeRepresentative y n v vRep) (hbound : ∀ᶠ (L : ℤ) in Filter.atTop, ∀ x ∈ V, uRep L x ≤ c) (hlim : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ((u L).toFun x - v.toFun x) ^ 2)) Filter.atTop (nhds 0)) {x : HCPolySupport.Vec d} (hx : x ∈ V) : vRep x ≤ c

A uniform bound on the truncated solutions' representatives passes to the representative of the L² limit, at every point of an open subset of the cube.

theorem Algsuperdiff.Section5.Support.ge_on_open_subset_of_tendsto_l2 {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {V : Set (HCPolySupport.Vec d)} (hVopen : IsOpen V) (hV : V ⊆ cubeSetAt y n) {u : ℤ → HCPolySupport.H1Function (cubeSetAt y n)} {uRep : ℤ → HCPolySupport.Vec d → ℝ} {v : HCPolySupport.H1Function (cubeSetAt y n)} {vRep : HCPolySupport.Vec d → ℝ} {c : ℝ} (hu : ∀ (L : ℤ), IsCubeRepresentative y n (u L) (uRep L)) (hv : IsCubeRepresentative y n v vRep) (hbound : ∀ᶠ (L : ℤ) in Filter.atTop, ∀ x ∈ V, c ≤ uRep L x) (hlim : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ((u L).toFun x - v.toFun x) ^ 2)) Filter.atTop (nhds 0)) {x : HCPolySupport.Vec d} (hx : x ∈ V) : c ≤ vRep x

The lower-bound form of the same transfer.