GammaTenEnvelopeInputGrid

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

The Besov envelope of Step 2, produced on the whole mesh at once

ABK26, Step 2 of l.approximate.recurrence.formula, e.lower.bound.oscillations.

The two obstructions this module removes

Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput asks for a family Bg of nonnegative sample functions, one per mesh cell, that dominates every finite-depth positive q = 2 Besov seminorm of the localized field on that cell almost surely, lies in L^4, and whose grid fourth-moment root is below cgamma^{15}. Two things stand between it and the proved machinery.

1. Closure.GammaTenEnvelope.exists_besovEnvelope_of_integral_pow_four_le produces an envelope from a per-cell fourth-moment bound, but the oscillation input of Step 2 is a grid average: reading a grid average at one cell costs the factor 3^{jd} and destroys the threshold. The fix is not to read the grid average at a cell at all: the envelope device is run simultaneously at every cell of the grid, and the fourth moments are compared only after the grid average has been taken.

2. The device needs the family it envelopes to be measurable in the sample, and the finite-depth Besov seminorm of the localized field is not known to be. The fix is to envelope a majorant instead: oscMajorant, built from the oscillation cells of e.nablaw.oscillations through cubeBesovPositiveVectorDepthAverage_le_descendantsAverage_sq. It dominates every finite-depth seminorm, is monotone in the depth cutoff, and its measurability and integrability reduce to those of meshOscillationCell, which are proved.

What is proved

• sq_sum_le_sum_two_pow_mul_sq --- the weighted Cauchy--Schwarz step (sum_i a_i)^2 <= sum_i 2^{i+1} a_i^2, the elementary replacement for Minkowski that the grid average tolerates.
• sq_descendantsAverage_le --- Jensen for the descendant average.
• exists_grid_pathwise_envelope_of_monotone --- the grid device: a monotone, measurable, nonnegative family indexed by the grid, whose grid average of fourth moments is bounded by a single C uniformly in the cutoff, admits a measurable pathwise envelope, cell by cell, in L^4, with the same grid average of fourth moments.
• oscMajorant, oscMajorant_nonneg, monotone_oscMajorant, measurable_oscMajorant --- the majorant and its three elementary properties.
• cubeBesovPositiveVectorPartialSeminormTwo_le_oscMajorant --- the domination, the only place the oscillation bridge is used.
• pow_four_oscMajorant_le --- the pointwise fourth-power bound: weighted Cauchy--Schwarz over depths, then Jensen inside each depth, leaving a weighted sum over depths of descendant averages of the fourth powers of the oscillation cells.
• integrable_descendantsAverage, integral_descendantsAverage, cubeFamilyAverage_finsetSum --- the commutations of the sample integral, the descendant average and the grid average that carry that pointwise bound to the grid average of the fourth moment of the majorant.
• sum_two_pow_mul_rpow_pow_four_geometric_le --- the geometric summation of the resulting weighted sum.

The fold at a grid family and the composite envelope itself are one step downstream, in Closure.GammaTenInteriorFamily (cubeFamilyAverage_integral_pow_four_oscMajorant_le_family and exists_besovEnvelope_of_family_depth_oscillation), whose per-depth input is read at the sub-family the consumer actually uses.

Binders

Measurability and fourth-power integrability of the oscillation cells in the sample, the L^2 membership of the field on the mesh cells' descendants, and the per-depth grid fourth-moment bounds. The first three are the standing integrability of the quantities being formed and are conditional A obligations of this module; the last is e.lower.bound.oscillations read at every depth of the tower. No smallness gate, no geometry beyond the triadic mesh, and nothing about the corrector or the coefficient field occurs.

Scope

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.lower.bound.oscillations, e.nablaw.oscillations.

Two elementary inequalities

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sq_sum_le_sum_two_pow_mul_sq (n : ℕ) (a : ℕ → ℝ) : (∑ i ∈ Finset.range n, a i) ^ 2 ≤ ∑ i ∈ Finset.range n, 2 ^ (i + 1) * a i ^ 2

Weighted Cauchy--Schwarz with summable weights. The square of a finite sum is below the sum of its squares weighted by 2^{i+1}; the weights are summable, which is the only property used. This is the elementary replacement for Minkowski in L^2 that survives the grid average unchanged.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sq_descendantsAverage_le {d : ℕ} (R : HCPolySupport.TriadicCube d) (i : ℕ) (F : HCPolySupport.TriadicCube d → ℝ) : HCPolySupport.descendantsAverage R i F ^ 2 ≤ HCPolySupport.descendantsAverage R i fun (R' : HCPolySupport.TriadicCube d) => F R' ^ 2

Jensen for the descendant average. Unconditional.

The grid envelope device

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_grid_pathwise_envelope_of_monotone {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (I : Finset (HCPolySupport.TriadicCube d)) (u : ℕ → HCPolySupport.TriadicCube d → Omega → ℝ) (hmeas : ∀ (N : ℕ), ∀ R ∈ I, Measurable (u N R)) (hnn : ∀ (N : ℕ) (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ u N R w) (hmono : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), Monotone fun (N : ℕ) => u N R w) (hint : ∀ (N : ℕ), ∀ R ∈ I, MeasureTheory.Integrable (fun (w : Omega) => u N R w ^ 4) mu) {C : ℝ} (hC : 0 ≤ C) (hbdd : ∀ (N : ℕ), (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∫ (w : Omega), u N R w ^ 4 ∂mu) ≤ C) : ∃ (B : HCPolySupport.TriadicCube d → Omega → ℝ), (∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ B R w) ∧ (∀ R ∈ I, Measurable (B R)) ∧ (∀ R ∈ I, ∀ᵐ (w : Omega) ∂mu, ∀ (N : ℕ), u N R w ≤ B R w) ∧ (∀ R ∈ I, MeasureTheory.MemLp (B R) 4 mu) ∧ (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∫ (w : Omega), B R w ^ 4 ∂mu) ≤ C

A monotone family indexed by the grid, with a uniform grid fourth moment, has a pathwise envelope carrying the same grid fourth moment.

The grid version of Closure.GammaTenEnvelope.exists_pathwise_envelope_of_monotone. The point is that the fourth moments are compared only after the grid average: no cell of the grid ever sees the grid average, so the 3^{jd} of a per-cell reading never appears. Monotone convergence is run inside the finite sum over the grid by ENNReal.finsetSum_iSup_of_monotone.

on measurability, nonnegativity and monotonicity of the family, on the standing integrability hint of the moments being formed, and on the uniform grid bound hbdd.

The oscillation majorant

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.oscMajorantSq {d : ℕ} (base : ℤ) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The square of the majorant: the Besov tower's own weights applied to the descendant averages of the squared oscillation cells of e.nablaw.oscillations, at the scales base - i.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.oscMajorant {d : ℕ} (base : ℤ) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The oscillation majorant of the finite-depth positive q = 2 Besov seminorm. It dominates the seminorm by the oscillation bridge, is monotone in the depth cutoff, and is measurable in the sample as soon as the oscillation cells are.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.oscMajorantSq_nonneg {d : ℕ} (base : ℤ) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ oscMajorantSq base s N u R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.oscMajorant_nonneg {d : ℕ} (base : ℤ) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ oscMajorant base s N u R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.monotone_oscMajorant {d : ℕ} (base : ℤ) (s : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : Monotone fun (N : ℕ) => oscMajorant base s N u R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_oscMajorant {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (base : ℤ) (s : ℝ) (N : ℕ) (R : HCPolySupport.TriadicCube d) (U : Omega → HCPolySupport.Vec d → HCPolySupport.Vec d) (hcell : ∀ i ∈ Finset.range (N + 1), ∀ R' ∈ HCPolySupport.descendantsAtDepth R i, Measurable fun (w : Omega) => meshOscillationCell (base - ↑i) (U w) R') : Measurable fun (w : Omega) => oscMajorant base s N (U w) R

Measurability of the majorant in the sample, from measurability of the oscillation cells alone.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorPartialSeminormTwo_le_oscMajorant {d : ℕ} (R : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : ∀ i ∈ Finset.range (N + 1), ∀ R' ∈ HCPolySupport.descendantsAtDepth R i, MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure R')) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R s N u ≤ oscMajorant R.scale s N u R

The majorant dominates the finite-depth positive q = 2 Besov seminorm.

This is the only place LocalizationFluctuationOscillationBridge is used: the depth-i term of the tower on R is at most the depth-i descendant average of the squared oscillation cells at scale R.scale - i.

on the L^2 memberships on the descendants, the standing integrability of the quantities being formed.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.pow_four_oscMajorant_le {d : ℕ} (base : ℤ) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : oscMajorant base s N u R ^ 4 ≤ ∑ i ∈ Finset.range (N + 1), 2 ^ (i + 1) * Real.rpow 3 (s * ↑i) ^ 4 * HCPolySupport.descendantsAverage R i fun (R' : HCPolySupport.TriadicCube d) => meshOscillationCell (base - ↑i) u R' ^ 4

The pointwise fourth-power bound: weighted Cauchy--Schwarz over depths followed by Jensen inside each depth. Unconditional.

Bookkeeping for the descendant average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_descendantsAverage {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (R : HCPolySupport.TriadicCube d) (i : ℕ) (f : HCPolySupport.TriadicCube d → Omega → ℝ) (hf : ∀ R' ∈ HCPolySupport.descendantsAtDepth R i, MeasureTheory.Integrable (f R') mu) : MeasureTheory.Integrable (fun (w : Omega) => HCPolySupport.descendantsAverage R i fun (R' : HCPolySupport.TriadicCube d) => f R' w) mu

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_descendantsAverage {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (R : HCPolySupport.TriadicCube d) (i : ℕ) (f : HCPolySupport.TriadicCube d → Omega → ℝ) (hf : ∀ R' ∈ HCPolySupport.descendantsAtDepth R i, MeasureTheory.Integrable (f R') mu) : ∫ (w : Omega), HCPolySupport.descendantsAverage R i fun (R' : HCPolySupport.TriadicCube d) => f R' w ∂mu = HCPolySupport.descendantsAverage R i fun (R' : HCPolySupport.TriadicCube d) => ∫ (w : Omega), f R' w ∂mu

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_finsetSum {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) {iota : Type u_2} (s : Finset iota) (F : iota → HCPolySupport.TriadicCube d → ℝ) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∑ i ∈ s, F i R) = ∑ i ∈ s, cubeFamilyAverage I (F i)

The geometric summation of the fold

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.rpow_three_pow_four_eq (s : ℝ) (i : ℕ) : Real.rpow 3 (s * ↑i) ^ 4 = Real.rpow 3 (4 * s) ^ i

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sum_two_pow_mul_rpow_pow_four_geometric_le {s A r : ℝ} (hA : 0 ≤ A) (hr : 0 ≤ r) (D : ℕ → ℝ) (hD : ∀ (i : ℕ), D i ≤ A * r ^ i) (hq : 2 * Real.rpow 3 (4 * s) * r ≤ 1 / 2) (N : ℕ) : ∑ i ∈ Finset.range (N + 1), 2 ^ (i + 1) * Real.rpow 3 (s * ↑i) ^ 4 * D i ≤ 4 * A

The fold is summable at a geometric per-depth input. If the depth-i grid fourth moment of the oscillation cells is below A r^i, and the ratio 2 . 3^{4 s} r is below 1/2, then the weighted sum of the fold is below 4 A uniformly in the depth cutoff. At the closure's own exponent s = gammaTenBesovExponent = 1/2 the factor 3^{4 s} is 9, so the gate reads 18 r <= 1/2, i.e. r <= 1/36; the display's own per-depth ratio is 3^{-4} once the fourth moment is taken, which is well inside it.