GammaTenStripEnvelopeTwoLeg

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

One Besov envelope for the two scaled legs of Step 2

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

What this module does

Closure.GammaTenCloserAssembly.ClosureBesovEnvelopeInput --- and its interior restatement Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput --- asks for one sample family Bg dominating the Besov towers of both legs of the gauged bfF_z, with gridFourthMomentRoot Bg <= cgamma^{15}. By cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential and ..._flux those two towers are |c_1| and |c_2| times the towers of two raw fields, the Dirichlet corrector gradient and the Neumann flux field, with

  c_1 = sqrt(sigma_0) . sqrt(shom_n)^{-1} ,   c_2 = sqrt(sigma_0)^{-1} . sqrt(shom_n) ,

both bounded by the gauge cap of e.shom.h.bounds. This module produces that single envelope from the two raw per-depth inputs, and closes the arithmetic: each leg is enveloped at the budget cgamma^{15} / (4 C_g) by exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const, the two envelopes are added, and the elementary constant 8^{1/4} <= 2 of LocalizationOscillationGridMoment.gridFourthMomentRoot_le_add_of_le still leaves the sum below cgamma^{15}:

  8^{1/4} ( |c_1| + |c_2| ) cgamma^{15} / (4 C_g)  <=  2 . 2 C_g . cgamma^{15} / (4 C_g)
                                                   =  cgamma^{15} .

The single numerical premise hthr : 200 (4 A C_g)^4 cgamma^4 <= 1 is what the constants cost: A is the per-depth constant of the two raw inputs (1 for the Dirichlet leg, 2 d for the flux leg after Closure.GammaTenDepthFluxOscillation), C_g the gauge cap. Both are dimension-only, so hthr is a threshold on cgamma alone.

What is proved

• exists_besovEnvelope_two_legs_interiorMesoCubeGrid --- the two-leg envelope, dominating |c_1| times the tower of the first field and |c_2| times the tower of the second, with grid fourth-moment root below cgamma^{15}.

Binders

Those of the one-leg composite --- the scale bookkeeping, the boundary gate and the three cellwise typing binders, now for each of the two fields --- together with 1 <= A, 1 <= C_g, the scalar bounds |c_1|, |c_2| <= C_g, the two per-depth inputs at the common constant A, and the single numerical threshold hthr. Nothing about the corrector, the coefficient field or the sample space 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.Fz.def.

The fourth power of an L^4 family is integrable

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_rpow_four_of_memLp_four {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {f : Omega → ℝ} (hf : MeasureTheory.MemLp f 4 mu) (hf0 : ∀ (w : Omega), 0 ≤ f w) : MeasureTheory.Integrable (fun (w : Omega) => f w ^ 4) mu

For a nonnegative family in L^4, the fourth power is integrable, in the rpow spelling the grid functional uses. Unconditional.

The two-leg envelope

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_besovEnvelope_two_legs_interiorMesoCubeGrid {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (hno : n ≤ outer) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) (U V : Omega → HCPolySupport.Vec d → HCPolySupport.Vec d) {gamma A Cg c1 c2 : ℝ} (hgamma0 : 0 < gamma) (hA1 : 1 ≤ A) (hCg1 : 1 ≤ Cg) (hthr : 200 * (4 * A * Cg) ^ 4 * gamma ^ 4 ≤ 1) (hc1 : |c1| ≤ Cg) (hc2 : |c2| ≤ Cg) (hmeasU : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), Measurable fun (w : Omega) => meshOscillationCell (n - ↑i) (U w) R') (hintU : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.Integrable (fun (w : Omega) => meshOscillationCell (n - ↑i) (U w) R' ^ 4) mu) (hmem2U : ∀ (w : Omega) (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.MemLp (U w) 2 (HCPolySupport.normalizedCubeMeasure R')) (hmeasV : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), Measurable fun (w : Omega) => meshOscillationCell (n - ↑i) (V w) R') (hintV : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.Integrable (fun (w : Omega) => meshOscillationCell (n - ↑i) (V w) R' ^ 4) mu) (hmem2V : ∀ (w : Omega) (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.MemLp (V w) 2 (HCPolySupport.normalizedCubeMeasure R')) (hdepthU : ∀ (i : ℕ), (gridFourthMomentRoot mu (interiorMesoCubeGrid d K (n - ↑i) (outer - 1)) fun (R' : HCPolySupport.TriadicCube d) (w : Omega) => meshOscillationCell (n - ↑i) (U w) R') ≤ A * (gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))) (hdepthV : ∀ (i : ℕ), (gridFourthMomentRoot mu (interiorMesoCubeGrid d K (n - ↑i) (outer - 1)) fun (R' : HCPolySupport.TriadicCube d) (w : Omega) => meshOscillationCell (n - ↑i) (V w) R') ≤ A * (gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))) : ∃ (B : HCPolySupport.TriadicCube d → Omega → ℝ), (∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ B R w) ∧ (∀ R ∈ interiorMesoCubeGrid d K n outer, MeasureTheory.MemLp (B R) 4 mu) ∧ gridFourthMomentRoot mu (interiorMesoCubeGrid d K n outer) B ≤ gamma ^ 15 ∧ ∀ R ∈ interiorMesoCubeGrid d K n outer, ∀ᵐ (w : Omega) ∂mu, ∀ (N : ℕ), |c1| * HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N (U w) ≤ B R w ∧ |c2| * HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N (V w) ≤ B R w

One envelope for the two scaled legs.

From two per-depth grid fourth-moment roots at the same constant A and the single numerical threshold hthr, a nonnegative sample family B, in L^4 at every cell of interiorMesoCubeGrid d K n outer, whose grid fourth-moment root is below cgamma^{15} and which dominates, almost surely and at every depth cutoff, |c_1| times the Besov tower of U and |c_2| times the Besov tower of V.

on the scale bookkeeping, the boundary gate hsmall, the threshold hthr, the two scalar caps, the six cellwise typing binders and the two per-depth inputs.