OscillationDecayAverage

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

Averaging toolkit for the arbitrary-gap oscillation estimate

The arbitrary-gap estimate behind e.nablaw.oscillations is proved by turning a pointwise interior bound for the gradient of a harmonic function into a mean-square bound on a concentric triadic cube. Three purely measure-theoretic steps are needed for that passage, and none of them is available in CoarseGraining:

1. Cauchy--Schwarz against the constant 1. The interior estimate produces the average of |grad u - c|, while the right-hand side of the target is the normalized L^2 deviation. The elementary inequality (avg_V |f - c|)^2 <= avg_V (f - c)^2 bridges the two. It is proved here from 0 <= int_V (|f - c| - t)^2 with the optimal t, so no L^p duality, Holder machinery or MemLp bookkeeping is used.
2. Mean recentring. meanSquareOscillationVecOn is the deviation from the volume average, whereas the pointwise bound is naturally centred at a fixed point of the cube. The variance identity int_V (f - c)^2 = int_V (f - avg_V f)^2 + |V| (avg_V f - c)^2 shows that the average is the minimizer, so any centre may be used.
3. Pointwise to mean-square. A uniform bound for vecNormSq (h - c) on V bounds meanSquareDeviationVecOn V h c by the same constant.

The remaining declarations are the two elementary facts about the concentric cube family that the pointwise step consumes: the centre belongs to the cube, the sup-norm diameter is 3^m, and a continuous function is integrable on it.

Contents

• mem_openCubeAtScale_self, norm_sub_le_of_mem_openCubeAtScale, integrableOn_openCubeAtScale_of_continuous -- the cube facts.
• sq_setIntegral_abs_le_mul_setIntegral_sq, sq_volumeAverage_abs_sub_le_meanSquareDeviationOn -- Cauchy--Schwarz.
• meanSquareDeviationOn_volumeAverage_le, meanSquareOscillationVecOn_le_meanSquareDeviationVecOn -- mean recentring.
• meanSquareDeviationVecOn_le_of_forall_vecNormSq_le -- pointwise to mean-square.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

Elementary facts about the concentric cube family

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mem_openCubeAtScale_self {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) : z ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m

The centre of a concentric triadic cube belongs to it.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.norm_sub_le_of_mem_openCubeAtScale {d : ℕ} {z : HCPolySupport.Vec d} {m : ℤ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m) (hy : y ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m) : ‖x - y‖ ≤ 3 ^ m

The sup-norm diameter of a concentric cube.

Vec d carries the sup norm, so two points of the cube of scale m differ by at most its side length 3^m. This is the gauge in which the convex mean-value inequality is applied on the cube.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.openCubeAtScale_subset_euclideanClosedBall_dim {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) : HCPolySupport.Book.Ch03.openCubeAtScale z m ⊆ HCPolySupport.euclideanClosedBall z ((↑d + 1) * 3 ^ m)

A concentric triadic cube is contained in a concentric Euclidean closed ball whose radius is an explicit polynomial in the dimension.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrableOn_openCubeAtScale_of_continuous {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) (z : HCPolySupport.Vec d) (m : ℤ) : MeasureTheory.IntegrableOn f (HCPolySupport.Book.Ch03.openCubeAtScale z m) MeasureTheory.volume

A continuous function is integrable on every concentric triadic cube.

Cauchy--Schwarz against the constant

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sq_setIntegral_abs_le_mul_setIntegral_sq {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f V MeasureTheory.volume) (hf2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x ^ 2) V MeasureTheory.volume) : (∫ (x : HCPolySupport.Vec d) in V, |f x|) ^ 2 ≤ (MeasureTheory.volume V).toReal * ∫ (x : HCPolySupport.Vec d) in V, f x ^ 2

Cauchy--Schwarz against 1.

(int_V |f|)^2 <= |V| int_V f^2, proved from the nonnegativity of int_V (|f| - t)^2 at the optimal t = (int_V |f|) / |V|.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sq_volumeAverage_abs_sub_le_meanSquareDeviationOn {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {f : HCPolySupport.Vec d → ℝ} {c : ℝ} (hf : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x - c) V MeasureTheory.volume) (hf2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (f x - c) ^ 2) V MeasureTheory.volume) : (HCPolySupport.volumeAverage V fun (x : HCPolySupport.Vec d) => |f x - c|) ^ 2 ≤ HCPolySupport.Book.Ch01.meanSquareDeviationOn V f c

Cauchy--Schwarz in average form.

The square of the average of |f - c| is dominated by the mean-square deviation of f from c. This is the step that converts the output of the interior gradient estimate, an L^1 average, into the normalized L^2 deviation which e.nablaw.oscillations displays.

Mean recentring

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationOn_volumeAverage_le {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {f : HCPolySupport.Vec d → ℝ} (c : ℝ) (hf : MeasureTheory.IntegrableOn f V MeasureTheory.volume) (hf2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x ^ 2) V MeasureTheory.volume) : HCPolySupport.Book.Ch01.meanSquareDeviationOn V f (HCPolySupport.volumeAverage V f) ≤ HCPolySupport.Book.Ch01.meanSquareDeviationOn V f c

The volume average minimizes the mean-square deviation.

int_V (f - c)^2 = int_V (f - avg_V f)^2 + |V| (avg_V f - c)^2, so recentring a mean-square deviation at the volume average can only decrease it. This is what lets a pointwise estimate centred at an arbitrary point of the cube be converted into a bound for meanSquareOscillationVecOn.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareOscillationVecOn_le_meanSquareDeviationVecOn {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {h : HCPolySupport.Vec d → HCPolySupport.Vec d} (c : HCPolySupport.Vec d) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => h x i) V MeasureTheory.volume) (hint2 : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => h x i ^ 2) V MeasureTheory.volume) : HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V h ≤ HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V h c

Mean recentring for the vector oscillation.

meanSquareOscillationVecOn V h <= meanSquareDeviationVecOn V h c for every centre c: the coordinatewise volume average minimizes each summand.

Pointwise to mean-square

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_le_of_forall_vecNormSq_le {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {h : HCPolySupport.Vec d → HCPolySupport.Vec d} {c : HCPolySupport.Vec d} {B : ℝ} (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (h x i - c i) ^ 2) V MeasureTheory.volume) (hbound : ∀ x ∈ V, HCPolySupport.vecNormSq (h x - c) ≤ B) : HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V h c ≤ B

A uniform pointwise bound bounds the mean-square deviation.