GammaTenStripAssembly

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

Step 2 from an interior-mesh cell fold plus the boundary strip

ABK26, Step 2 of l.approximate.recurrence.formula, target e.lower.bound.localization.terms.

What this module is

Closure.GammaTenAssemblyBridge.fluctuationEnergyAverage_le_of_cell_fold and its grid-load mirror Closure.GammaTenCloserAssembly both consume the per-cell fold bound at every cell of the mesh descendantsAtDepth (cu_{Kc}) j. The interior route of Closure.GammaTenInterior* and Closure.GammaTenStripEnvelope supplies the Besov envelope, hence the per-cell fold bound, only on the interior mesh interiorMesoCubeGrid d Kc (Kc - j) outer --- the carrier forces, and the depth refinement of Closure.GammaTenInteriorGeometry.mem_interiorMesoCubeGrid_of_mem_descendantsAtDepth preserves.

This module is the passage from the one to the other. The full mesh splits into the interior mesh and the boundary strip; the strip is handled by the signed Cauchy--Schwarz transfer Closure.GammaTenStripTransfer.cubeFamilyAverage_mesoCubeGrid_le_max_interior_add, whose remainder is sqrt(d 3^{g-p}) times the square root of the full-mesh average of the squared cell expectations. That last quantity is the module's one exposed binder, hstrip.

What is proved

• cubeFamilyAverage_integral_fold_le_of_memLp_four_grid_load --- the grid Hoelder fold of Step 2 at an arbitrary family I of cells, with the load leg on the grid and the right-hand side a free target. The analytic content is Closure.GammaTenLoadFold.cubeFamilyAverage_integral_fold_le_gridLoad, which is already stated at an arbitrary Finset (TriadicCube d); its eight side conditions are discharged from the three L^4 legs by Closure.GammaTenAssemblyMoments, and the closing step uses hthr only.
• fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load --- the strip bridge: fluctuationEnergyAverage <= cgamma^{10} from
  • the per-cell fold bound hcell on the interior mesh only,
  • the three L^4 legs and the three moment bounds on the interior mesh only,
  • the numerical gate hthr at a free target,
  • the strip second moment hstrip, and
  • the absorption gate hgate, target + sqrt(d 3^{g-p}) sqrt(Cstrip) <= cgamma^{10}. As in the proved bridge, no integrability or measurability of the cell integrand itself is assumed: integral_mono_ae where it is integrable and integral_undef where it is not.

The residual this module isolates

hstrip is the only thing the interior route still owes beyond the interior Besov envelope. Stated in full, at the closure's own data, it is

  cubeFamilyAverage (mesoCubeGrid d Kc (Kc - j))
    (fun R => (integral_omega meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega
                 d(cutoffSampleLaw M))^2)
    <= Cstrip

with Cstrip independent of Kc --- or, since the consumer quantifies Kc through Filter.atTop after M, n, h, merely independent of the strip fraction, which tends to 0 as Kc -> infinity. This module does not prove it and does not hide it.

Binders

The scale bookkeeping Kc = (Kc - j) + p, outer + 1 = (Kc - j) + g, g <= p; pointwise nonnegativity and interior-mesh L^4 membership of the three legs; the three interior-mesh moment bounds; hthr, hcell, hstrip, hgate and 0 <= target. No smallness gate on cgamma is imposed beyond what hthr and hgate state.

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.localization.terms, e.recurrence.params.

The grid Hoelder fold at an arbitrary family

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_integral_fold_le_of_memLp_four_grid_load {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (I : Finset (HCPolySupport.TriadicCube d)) (F G H : HCPolySupport.TriadicCube d → Omega → ℝ) (hF : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ F R w) (hG : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ G R w) (hH : ∀ (R : HCPolySupport.TriadicCube d) (w : Omega), 0 ≤ H R w) (hF4 : ∀ R ∈ I, MeasureTheory.MemLp (F R) 4 mu) (hG4 : ∀ R ∈ I, MeasureTheory.MemLp (G R) 4 mu) (hH4 : ∀ R ∈ I, MeasureTheory.MemLp (H R) 4 mu) {gamma Cload c1 c2 target : ℝ} (hgamma : 0 < gamma) (hc1 : 0 ≤ c1) (hc2 : 0 ≤ c2) (hell : ∀ R ∈ I, ∫ (w : Omega), F R w ^ 4 ∂mu ≤ (gamma ^ 8)⁻¹) (hload : gridFourthMomentRoot mu I G ≤ Cload) (hosc : gridFourthMomentRoot mu I H ≤ gamma ^ 15) (hthr : ∀ (Bosc : ℝ), 0 ≤ Bosc → Bosc ≤ gamma ^ 15 → c1 * Cload * ((gamma ^ 2)⁻¹ * Bosc) + c2 * ((gamma ^ 2)⁻¹ * Bosc ^ 2) ≤ target) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∫ (w : Omega), c1 * (F R w * G R w * H R w) + c2 * (F R w * H R w * H R w) ∂mu) ≤ target

The Step-2 grid Hoelder fold at an arbitrary family of cells, with the load leg on the grid and a free right-hand side.

The Step-2 grid fold at an arbitrary I : Finset (TriadicCube d) rather than a full descendant mesh, and with cgamma^{10} replaced by whatever target the numerical gate hthr delivers. Neither generalization touches the proof: the analytic content is Closure.GammaTenLoadFold.cubeFamilyAverage_integral_fold_le_gridLoad, which is already stated at an arbitrary family, and target occurs only in the closing step.

on the pointwise nonnegativity of the three legs, their L^4 membership at each cell of I, the three moment bounds on I and the numerical gate.

The strip bridge

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) {outer : ℤ} {p g : ℕ} (hKp : Kc = Kc - ↑j + ↑p) (houter : outer + 1 = Kc - ↑j + ↑g) (hgp : g ≤ p) (F G H : HCPolySupport.TriadicCube d → Cutoff.CutoffSample d → ℝ) (hF : ∀ (R : HCPolySupport.TriadicCube d) (w : Cutoff.CutoffSample d), 0 ≤ F R w) (hG : ∀ (R : HCPolySupport.TriadicCube d) (w : Cutoff.CutoffSample d), 0 ≤ G R w) (hH : ∀ (R : HCPolySupport.TriadicCube d) (w : Cutoff.CutoffSample d), 0 ≤ H R w) (hF4 : ∀ R ∈ interiorMesoCubeGrid d Kc (Kc - ↑j) outer, MeasureTheory.MemLp (F R) 4 ↑(Cutoff.cutoffSampleLaw M)) (hG4 : ∀ R ∈ interiorMesoCubeGrid d Kc (Kc - ↑j) outer, MeasureTheory.MemLp (G R) 4 ↑(Cutoff.cutoffSampleLaw M)) (hH4 : ∀ R ∈ interiorMesoCubeGrid d Kc (Kc - ↑j) outer, MeasureTheory.MemLp (H R) 4 ↑(Cutoff.cutoffSampleLaw M)) {Cload c1 c2 target Cstrip : ℝ} (hc1 : 0 ≤ c1) (hc2 : 0 ≤ c2) (htarget0 : 0 ≤ target) (hell : ∀ R ∈ interiorMesoCubeGrid d Kc (Kc - ↑j) outer, ∫ (w : Cutoff.CutoffSample d), F R w ^ 4 ∂↑(Cutoff.cutoffSampleLaw M) ≤ (M.gamma ^ 8)⁻¹) (hload : gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d Kc (Kc - ↑j) outer) G ≤ Cload) (hosc : gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d Kc (Kc - ↑j) outer) H ≤ M.gamma ^ 15) (hthr : ∀ (Bosc : ℝ), 0 ≤ Bosc → Bosc ≤ M.gamma ^ 15 → c1 * Cload * ((M.gamma ^ 2)⁻¹ * Bosc) + c2 * ((M.gamma ^ 2)⁻¹ * Bosc ^ 2) ≤ target) (hcell : ∀ R ∈ interiorMesoCubeGrid d Kc (Kc - ↑j) outer, ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega ≤ c1 * (F R omega * G R omega * H R omega) + c2 * (F R omega * H R omega * H R omega)) (hstrip : (cubeFamilyAverage (mesoCubeGrid d Kc (Kc - ↑j)) fun (R : HCPolySupport.TriadicCube d) => (∫ (omega : Cutoff.CutoffSample d), meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega ∂↑(Cutoff.cutoffSampleLaw M)) ^ 2) ≤ Cstrip) (hgate : target + √(↑d * (3 ^ g / 3 ^ p)) * √Cstrip ≤ M.gamma ^ 10) : fluctuationEnergyAverage M n h Kc j e e' wD wN ≤ M.gamma ^ 10

Step 2 at one localization scale, from a fold bound on the interior mesh only.

  fluctuationEnergyAverage  =  avsum_{R in mesh} E[ fluct_R ]
      <=  target  +  sqrt(d 3^{g-p}) . sqrt(Cstrip)  <=  cgamma^{10} ,

the first inequality being the signed Cauchy--Schwarz split of Closure.GammaTenStripTransfer.cubeFamilyAverage_mesoCubeGrid_le_max_interior_add and the interior average being folded by cubeFamilyAverage_integral_fold_le_of_memLp_four_grid_load. The cell integrand has no sign, which is why the signed split is needed; only its interior values are ever compared with the majorant.

As in Closure.GammaTenAssemblyBridge.fluctuationEnergyAverage_le_of_cell_fold, no integrability and no measurability of the cell integrand is assumed: integral_mono_ae where it is integrable, integral_undef where it is not.