ClosureInteriorSplit

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

ClosureSplitInput from an interior-mesh oscillation envelope plus the strip

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

What this module composes

Step 2 at the closure's own corrector families runs off a Besov envelope on the full mesh descendantsAtDepth (cu_K) j. The interior route of Closure.GammaTenInterior* and Closure.GammaTenStripEnvelope produces the envelope only on the interior mesh interiorMesoCubeGrid d K (K - j) n --- the carrier forces --- and Closure.GammaTenStripAssembly.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load is the bridge from the one to the other, at the price of two exposed binders: the strip second moment and its absorption gate.

This module runs Step 2 through that bridge, so the envelope may be read on the interior mesh throughout. The two carrier-facing points are:

• the load leg's grid fourth-moment root, which Closure.GammaTenLoad.exists_gammaTenLoadConst_root delivers on the full mesh, is moved to the interior mesh by gridFourthMomentRoot_interiorMesoCubeGrid_le at the cost of the absolute factor 3^d;
• the numerical gate is produced at the doubled absolute constants, so that the folded interior average is below cgamma^{10} / 2 and the strip remainder has the other half to live in.

The window scale, and the two parameters the bridge needs

The bridge's scale bookkeeping is K = (K - j) + p, outer + 1 = (K - j) + g, g <= p. At the closure's own data these are forced:

  K - j = recurrenceMesoScale 32 cgamma (n + h) h = n - recurrenceGap 32 cgamma ,
  p = j ,   outer = n ,   g = closureStripGap M = recurrenceGap 32 cgamma + 1 ,

outer = n being exactly the window scale at which exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const produces the interior envelope, one larger than the depth endpoints' own n - 1. g <= p and the two largeness gates hold for every sufficiently large localization cube.

What is proved

• gridFourthMomentRoot_interiorMesoCubeGrid_le --- the full-mesh to interior-mesh transfer of a grid fourth-moment root, at the factor 3^d of LocalizationGrid.cubeFamilyAverage_interior_le_of_full.
• gammaTenBound_of_interiorEnvelope --- Step 2 at the closure's families, i.e. the verbatim antecedent of Closure.SplitFoldIntegrability.closureSplitInput_of_gammaTenBound, from the two named inputs below.
• closureSplitInput_of_interiorEnvelope --- Closure.ClosureFinal.ClosureSplitInput from the same two inputs.

The two named inputs, and their status

ClosureInteriorBesovEnvelopeInput and ClosureStripRemainder are conditional A obligations of this module; neither is proved here.

• ClosureInteriorBesovEnvelopeInput is the manuscript's own e.lower.bound.oscillations, read at the Besov tower of the gauged bfF_z on the interior mesh at window scale n. The depth-indexed interior endpoints from Closure.GammaTenDepthOscillation for the Dirichlet and Neumann correctors and the envelope device exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const are the route to it, taken downstream in Closure.GammaTenInteriorHosc.closureInteriorBesovEnvelopeInput_proved; that composition is not performed here and the input is carried explicitly.
• ClosureStripRemainder is the boundary-strip residual that Closure.GammaTenStripAssembly isolates and does not prove (its module header, "The residual this module isolates"): a second-moment bound on the full mesh together with the absorption of sqrt(d 3^{g-p}) times its square root into half of cgamma^{10}.

Binders

The two named inputs and the standing 2 <= d. No smallness gate on cgamma, no measurability of the cell integrand and no integrability of the Step-2 integrand is assumed; every threshold is produced.

Scope

Internal Provider infrastructure. 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.lower.bound.oscillations, e.recurrence.params.

The full-mesh to interior-mesh transfer of a grid fourth-moment root

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gridFourthMomentRoot_interiorMesoCubeGrid_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (d : ℕ) {K nmesh outer : ℤ} (hn : nmesh ≤ K - 1) (houter : outer + 1 ≤ K - 1) (F : HCPolySupport.TriadicCube d → Omega → ℝ) {C : ℝ} (hC : 0 ≤ C) (hroot : gridFourthMomentRoot mu (mesoCubeGrid d K nmesh) F ≤ C) : gridFourthMomentRoot mu (interiorMesoCubeGrid d K nmesh outer) F ≤ 3 ^ d * C

A grid fourth-moment root survives the passage to the interior mesh, at the absolute factor 3^d.

The interior mesh is a subfamily of the full mesh whose cardinality is at least 3^{-d} of it (LocalizationGrid.card_mesoCubeGrid_le_three_pow_mul_card_interior), so the interior average of the nonnegative cell fourth moments is at most 3^d times the full one. Unconditional beyond the two scale gates and 0 <= C.

The two named inputs of the interior route

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureStripGap {d : ℕ} (M : ABKModel d) : ℕ

The boundary-strip gap of the closure's own mesh: with the mesh scale K - j = n - recurrenceGap 32 cgamma and window scale outer = n, the bridge's outer + 1 = (K - j) + g forces g = recurrenceGap 32 cgamma + 1.

Equations

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

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureInteriorBesovEnvelopeInput (d : ℕ) [NeZero d] : Prop

The residual oscillation input of Step 2, on the interior mesh.

The residual oscillation obligation of Step 2, stated not on the full mesh descendantsAtDepth (cu_K) (closureMeshDepth M n h K) but on the interior mesh interiorMesoCubeGrid d K (K - closureMeshDepth M n h K) n at window scale n, which is the carrier the interior route of Closure.GammaTenInterior* and Closure.GammaTenStripEnvelope produces. Everything else --- the exponent gammaTenBesovExponent = 1/2, the gauge shom_{n+h-1}, the two legs of the gauged bfF_z, the L^4 membership and the cgamma^{15} root --- is unchanged.

It is a conditional A obligation of this module and is not proved here.

Equations

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

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureStripRemainder (d : ℕ) [NeZero d] : Prop

The boundary-strip residual of the interior route.

At the closure's own families, for all sufficiently large localization cubes, a bound Cstrip on the full-mesh average of the squared cell expectations of the Step-2 integrand, together with the absorption of the signed Cauchy--Schwarz remainder sqrt(d 3^{g-p}) sqrt(Cstrip) into half of cgamma^{10}. The Filter.atTop quantifier is exactly the one the consumer uses, so nothing is asked for at a cube the consumer does not reach.

This is exactly what Closure.GammaTenStripAssembly isolates as hstrip and hgate and does not prove; see that module's header. It is a conditional A obligation of this module and is not proved here.

Equations

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

Step 2 from the two inputs

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenBound_of_interiorEnvelope (d : ℕ) [NeZero d] (hd : 2 ≤ d) (hosc : ClosureInteriorBesovEnvelopeInput d) (hstrip : ClosureStripRemainder d) : ∃ (Cfl : ℝ), 0 < Cfl ∧ ∀ (M : ABKModel d) (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }) (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ClosureRegime Cfl M n h Ec → ∀ᶠ (K : ℕ) in Filter.atTop, fluctuationEnergyAverage M n h (↑K) (closureMeshDepth M n h K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') ≤ M.gamma ^ 10

Step 2 at the closure's own corrector families, through the strip bridge, i.e. the verbatim antecedent of Closure.SplitFoldIntegrability.closureSplitInput_of_gammaTenBound.

exactly on ClosureInteriorBesovEnvelopeInput d, ClosureStripRemainder d and the standing 2 <= d.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureSplitInput_of_interiorEnvelope (d : ℕ) [NeZero d] (hd : 2 ≤ d) (hosc : ClosureInteriorBesovEnvelopeInput d) (hstrip : ClosureStripRemainder d) : ClosureSplitInput d

Closure.ClosureFinal.ClosureSplitInput from the interior-mesh envelope and the strip residual.