GammaTenInteriorCellInputs

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

The cellwise typing inputs of the interior envelope, at the closure's families

ABK26, e.nablaw.oscillations, e.Fz.def, e.def.w, e.nablaw.in.L.eight.

What this module supplies

The interior Besov envelope of Closure.GammaTenInteriorGaugedEnvelope carries, for each of its two raw legs, the three cellwise typing binders

  Measurable (osc cell) ,   Integrable ((osc cell)^4) ,   MemLp (field) 2 ,

read at every depth-refined interior grid. Each is a statement about one cell, and the only spatial data a cell of the interior grid carries is its scale and its containment in the localization cube. This module produces the six at the closure's own Dirichlet and Neumann families, from the single L^8 membership of the two corrector gradients:

• the Dirichlet leg's measurability is the proved Closure.Step5InputOscillation.measurable_meshOscillationCell_freshShellDirichletGrad, composed with the sample inclusion;
• the flux leg's is Closure.GammaTenFluxMeasurability.measurable_meshOscillationCell_neumannFluxField_cutoffSample;
• the flux leg's fourth-power integrability is the Dirichlet-style one for the Neumann gradient plus integrable_meshOscillationCell_pow_four_neumannFluxField_cutoffSample;
• the two L^2 memberships are the proved Closure.GammaTenAssemblySide.memLp_two_gradH10_normalizedCubeMeasure_of_subset and ..._neumannFluxField_normalizedCubeMeasure.

What is proved

• memLp_eight_neumannFluxField_closure --- the flux leg is L^8 on the localization cube, the gradient by e.nablaw.in.L.eight and the forcing because it is continuous.
• measurable_meshOscillationCell_closureDirichlet_cutoffSample and measurable_meshOscillationCell_closureFlux_cutoffSample --- the two measurabilities at one cell.
• integrable_meshOscillationCell_pow_four_closureFlux_cutoffSample --- the flux leg's fourth-power integrability at one cell, from the Neumann gradient's.

Binders

The standing 2 <= d, the cell data hsc : R.scale = nn and hsub : openCubeSet R ⊆ openCubeSet (cu_K), the scale gate nn <= n and n < n + h for the integrability, and --- for the integrability only --- the Neumann gradient cell's own fourth-power integrability. No smallness gate on cgamma and no model estimate 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, e.nablaw.oscillations, e.Fz.def, e.def.w, e.nablaw.in.L.eight.

The flux leg is L^8 on the localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.memLp_eight_neumannFluxField_closure {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : MeasureTheory.MemLp (neumannFluxField (Annealed.sigmaBar M n) omega n (n + ↑h) e' (closureNeumannAlong M n h K e' omega)) 8 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d ↑K))

The flux leg of e.Fz.def is L^8 on cu_K. The gradient by e.nablaw.in.L.eight, the stream forcing because it is continuous.

Proved from memLp_eight_grad_closureNeumannAlong.

Measurability of the two oscillation cells

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_meshOscillationCell_closureDirichlet_cutoffSample {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) {nn : ℤ} (R : HCPolySupport.TriadicCube d) (hsc : R.scale = nn) (hsub : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) : Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell nn (closureDirichletAlong M n h K e ↑omega).grad R

The Dirichlet leg's oscillation cell is measurable on the cutoff-sample carrier.

Conditional on hd and the cell data hsc, hsub.

Proved from memLp_eight_grad_closureDirichletAlong.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_meshOscillationCell_closureFlux_cutoffSample {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) {nn : ℤ} (R : HCPolySupport.TriadicCube d) (hsc : R.scale = nn) (hsub : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) : Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell nn (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R

The flux leg's oscillation cell is measurable on the cutoff-sample carrier.

Conditional on hd and the cell data hsc, hsub.

Proved from memLp_eight_grad_closureNeumannAlong.

The flux leg's fourth-power integrability

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_meshOscillationCell_pow_four_closureFlux_cutoffSample {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) (hh : 0 < h) {nn : ℤ} (hnn : nn ≤ n) (R : HCPolySupport.TriadicCube d) (hsc : R.scale = nn) (hsub : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (hoscInt : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell nn (closureNeumannAlong M n h K e' ↑omega).toH1Function.grad R ^ 4) ↑(Cutoff.cutoffSampleLaw M)) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell nn (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R ^ 4) ↑(Cutoff.cutoffSampleLaw M)

The flux leg's hintcell at one cell, from the Neumann gradient's.

Conditional on hd, the scale gates hnn, hh, the cell data hsc, hsub, and the Neumann gradient cell's own fourth-power integrability hoscInt.

Proved from memLp_eight_grad_closureNeumannAlong through the measurability.