GammaTenInteriorHosc

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

ClosureInteriorBesovEnvelopeInput, produced

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

What this module does

Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput is the conditional A obligation the interior route of Closure.ClosureInteriorSplit carries and does not prove. This module discharges it, by the composition the ClosureInteriorSplit header names:

• the depth-indexed interior endpoints from Closure.GammaTenDepthOscillation for the Dirichlet and Neumann correctors supply the two per-depth grid roots, the Neumann one through the flux transport gridFourthMomentRoot_meshOscillationCell_neumannFluxField_cutoffSample_le (cost: the explicit dimensional factor 2 d);
• the envelope device Closure.GammaTenStripEnvelopeTwoLeg.exists_besovEnvelope_two_legs_interiorMesoCubeGrid, read through the gauge substitution of Closure.GammaTenInteriorGaugedEnvelope, turns them into one envelope for the two gauged legs of bfF_z;
• the cellwise typing data comes from Closure.GammaTenInteriorCellInputs and the octic layer from LocalizationFluctuationNumericOctic for both corrector fields;
• the scale bookkeeping is the closure's own, exactly as Closure.ClosureInteriorSplit.gammaTenBound_of_interiorEnvelope computes it, and the boundary gate is Closure.GammaTenInteriorGeometry.exists_gamma_threshold_mesh_boundary_half at p = closureMeshDepth, g = closureStripGap.

Every threshold on cgamma is produced before the model and collected into the single constant the obligation quantifies, through Closure.SplitObligationsRegime.gamma_le_of_closureRegime; the only genuinely new numerical threshold is the two-leg envelope's 200 (4 . 2d . 4 . 3^9)^4 cgamma^4 <= 1, which is dimension-only.

What is proved

• le_of_add_le_of_nonneg_right, integrable_pow_four_cutoffSample_of_memLp_two_rpow, integrable_rpow_four_cutoffSample_of_memLp_two_rpow --- three small bridges.
• exists_gamma0_octicCell_closureDirichlet, ..._closureNeumann --- the octic layer, read at the closure's own families.
• exists_gamma0_depthRoot_closureDirichlet, ..._closureNeumann --- the two depth endpoints, read at the closure's own families and mesh scale.
• exists_besovEnvelope_closureInterior_of_inputs --- the body of the obligation at one localization cube and an abstract mesh scale, from those four inputs.
• closureInteriorBesovEnvelopeInput_proved --- the obligation itself.

Binders

Of the terminal statement: the standing 2 <= d alone. Everything else --- the five cgamma thresholds, the large-cube gate, the depth-naming identity and the strip-gap bookkeeping --- is produced inside the manuscript's own parameter block ClosureRegime.

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.oscillations, e.nablaw.oscillations, e.Fz.def, e.recurrence.params, e.shom.h.bounds.

Three small bridges

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.le_of_add_le_of_nonneg_right {A B C : ℝ} (hB : 0 ≤ B) (h : A + B ≤ C) : A ≤ C

Dropping a nonnegative summand on the smaller side.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_pow_four_cutoffSample_of_memLp_two_rpow {d : ℕ} (M : ABKModel d) {F : Cutoff.ShellSeq d → ℝ} (hmem : MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => F omega ^ 4) 2 ↑M.P) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => F ↑omega ^ 4) ↑(Cutoff.cutoffSampleLaw M)

The octic layer's L^2 membership of the fourth power of a shell observable gives that fourth power's integrability on the closure's carrier, in the natural power spelling the envelope's hintcell uses.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_rpow_four_cutoffSample_of_memLp_two_rpow {d : ℕ} (M : ABKModel d) {F : Cutoff.ShellSeq d → ℝ} (hmem : MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => F omega ^ 4) 2 ↑M.P) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => F ↑omega ^ 4) ↑(Cutoff.cutoffSampleLaw M)

The same in the rpow spelling the grid Minkowski step uses.

The octic layer at the closure's families

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_octicCell_closureDirichlet (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (n + ↑h - 1) Ec → 0 < h → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → ∀ (K : ℕ), 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (closureDirichletAlong M n h K e omega).grad R ^ 4) 2 ↑M.P

The octic cell membership at the closure's Dirichlet family.

The proved exists_gamma0_memLp_two_freshShellDirichlet_meshOscillationCell_rpow_four, with its six spatial side conditions discharged from the single L^8 membership of the closure's corrector gradient.

Proved from that producer and memLp_eight_grad_closureDirichletAlong.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_octicCell_closureNeumann (d : ℕ) (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (n + ↑h - 1) Ec → 0 < h → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → ∀ (K : ℕ), 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → ∀ (e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (closureNeumannAlong M n h K e' omega).toH1Function.grad R ^ 4) 2 ↑M.P

The octic cell membership at the closure's Neumann family. The Neumann mirror of the preceding statement.

Proved as above, through memLp_eight_grad_closureNeumannAlong.

The two depth endpoints at the closure's families

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_depthRoot_closureDirichlet (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (n + ↑h - 1) Ec → 0 < h → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → ∀ (K : ℕ), 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → ∀ (nmesh : ℤ), nmesh = recurrenceMesoScale recurrenceGapMultiplier M.gamma (n + ↑h) ↑h → ∀ (i : ℕ), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e omega).grad R') ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))

The Dirichlet depth root at the closure's family, with the additive forcing gauge of the endpoint dropped.

Proved from exists_gamma0_freshShellDirichlet_meshOscillationDepth_le_gamma_pow_sixteen.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_depthRoot_closureNeumann (d : ℕ) (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (n + ↑h - 1) Ec → 0 < h → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → ∀ (K : ℕ), 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → ∀ (e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (nmesh : ℤ), nmesh = recurrenceMesoScale recurrenceGapMultiplier M.gamma (n + ↑h) ↑h → ∀ (i : ℕ) (z0 : HCPolySupport.Vec d), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureNeumannAlong M n h K e' omega).toH1Function.grad R') + (↑(Annealed.sigmaBar M n))⁻¹ * (3 ^ ↑(nmesh - ↑i) * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum n (n + ↑h) z0 omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))

The Neumann depth endpoint at the closure's family, in the exact shape the flux transport's hend binder asks for --- gradient root plus forcing gauge, at every base point.

Proved from exists_gamma0_freshShellNeumann_meshOscillationDepth_le_gamma_pow_sixteen.

The eight inputs of the two-leg envelope, one theorem each

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.scale_and_subset_of_mem_interiorMesoCubeGrid {d : ℕ} {K nmesh outer : ℤ} (hnK : nmesh ≤ K) {R' : HCPolySupport.TriadicCube d} (hR' : R' ∈ interiorMesoCubeGrid d K nmesh outer) : R'.scale = nmesh ∧ HCPolySupport.openCubeSet R' ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

A cell of an interior meso grid below the localization scale carries exactly two pieces of spatial data: its scale, and its containment in cu_K.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_oscCell_closureDirichlet_grid (d : ℕ) [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (i : ℕ) (R' : HCPolySupport.TriadicCube d) : R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1) → Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e ↑omega).grad R'

hmeascell for the Dirichlet leg, at every depth-refined interior grid.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_oscCell_closureFlux_grid (d : ℕ) (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (i : ℕ) (R' : HCPolySupport.TriadicCube d) : R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1) → Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R'

hmeascell for the flux leg, at every depth-refined interior grid.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_oscCell_pow_four_grid_of_octic {d : ℕ} (M : ABKModel d) (n : ℤ) (K : ℕ) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (u : Cutoff.ShellSeq d → HCPolySupport.Vec d → HCPolySupport.Vec d) (hoct : ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (u omega) R ^ 4) 2 ↑M.P) (i : ℕ) (R' : HCPolySupport.TriadicCube d) : R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1) → MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (u ↑omega) R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)

hintcell for a corrector gradient leg, at every depth-refined interior grid, from the octic membership. Stated for a general family so that both legs use it.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_oscCell_rpow_four_grid_of_octic {d : ℕ} (M : ABKModel d) (n : ℤ) (K : ℕ) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (u : Cutoff.ShellSeq d → HCPolySupport.Vec d → HCPolySupport.Vec d) (hoct : ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (u omega) R ^ 4) 2 ↑M.P) (i : ℕ) (R' : HCPolySupport.TriadicCube d) : R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1) → MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (u ↑omega) R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)

The rpow spelling of the same, which is what the flux transport asks for.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_oscCell_pow_four_closureFlux_grid (d : ℕ) (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) (hhpos : 0 < h) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (hnmn : nmesh ≤ n) (hgrad : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureNeumannAlong M n h K e' ↑omega).toH1Function.grad R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)) (i : ℕ) (R' : HCPolySupport.TriadicCube d) : R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1) → MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)

hintcell for the flux leg, at every depth-refined interior grid.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.depthRoot_cutoffSample_closureDirichlet (d : ℕ) [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) {nmesh : ℤ} (hdepD : ∀ (i : ℕ), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e omega).grad R') ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))) (i : ℕ) : (gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e ↑omega).grad R') ≤ 2 * ↑d * (M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))

The Dirichlet per-depth grid root on the closure's carrier, at the common constant 2 d.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.depthRoot_cutoffSample_closureFlux (d : ℕ) (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) (he' : HCPolySupport.Book.Ch02.vecNorm e' ≤ 1) (hhpos : 0 < h) {nmesh : ℤ} (hnK : nmesh ≤ ↑K) (hnmn : nmesh ≤ n) (hoscInt : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureNeumannAlong M n h K e' ↑omega).toH1Function.grad R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)) (hdepN : ∀ (i : ℕ) (z0 : HCPolySupport.Vec d), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureNeumannAlong M n h K e' omega).toH1Function.grad R') + (↑(Annealed.sigmaBar M n))⁻¹ * (3 ^ ↑(nmesh - ↑i) * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum n (n + ↑h) z0 omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))) (i : ℕ) : (gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R') ≤ 2 * ↑d * (M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))

The flux per-depth grid root on the closure's carrier, at the constant 2 d the flux transport costs.

The obligation's body at one localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_besovEnvelope_closureInterior_of_inputs (d : ℕ) [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) (he' : HCPolySupport.Book.Ch02.vecNorm e' ≤ 1) (hgamma0 : 0 < M.gamma) (hhpos : 0 < h) {nmesh : ℤ} {p g : ℕ} (hKp : ↑K = nmesh + ↑p) (houter : n + 1 = nmesh + ↑g) (hgp : g ≤ p) (hno : nmesh ≤ n) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) (hthr : 200 * (4 * (2 * ↑d) * (4 * 3 ^ 9)) ^ 4 * M.gamma ^ 4 ≤ 1) (hgauge : gaugeRatio (Annealed.sigmaBar M n) (Annealed.sigmaBar M (n + ↑h - 1)) ≤ 4 * 3 ^ 9) (hoctD : ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (closureDirichletAlong M n h K e omega).grad R ^ 4) 2 ↑M.P) (hoctN : ∀ (nn : ℤ) (R : HCPolySupport.TriadicCube d), R.scale = nn → HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => meshOscillationCell nn (closureNeumannAlong M n h K e' omega).toH1Function.grad R ^ 4) 2 ↑M.P) (hdepD : ∀ (i : ℕ), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e omega).grad R') ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))) (hdepN : ∀ (i : ℕ) (z0 : HCPolySupport.Vec d), (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (nmesh - ↑i) (closureNeumannAlong M n h K e' omega).toH1Function.grad R') + (↑(Annealed.sigmaBar M n))⁻¹ * (3 ^ ↑(nmesh - ↑i) * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum n (n + ↑h) z0 omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i))) : ∃ (Bg : HCPolySupport.TriadicCube d → Cutoff.CutoffSample d → ℝ), (∀ (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d), 0 ≤ Bg R omega) ∧ (∀ R ∈ interiorMesoCubeGrid d (↑K) nmesh n, MeasureTheory.MemLp (Bg R) 4 ↑(Cutoff.cutoffSampleLaw M)) ∧ gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) nmesh n) Bg ≤ M.gamma ^ 15 ∧ ∀ R ∈ interiorMesoCubeGrid d (↑K) nmesh n, ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).1) ≤ Bg R omega) ∧ ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).2) ≤ Bg R omega

The body of ClosureInteriorBesovEnvelopeInput at one localization cube.

Stated at an abstract mesh scale nmesh and abstract strip parameters p, g, so that no arithmetic definition has to be unfolded. The four named inputs are exactly what the four producers above deliver.

Conditional on hd, he', hgamma0, hhpos, the scale bookkeeping, the boundary gate hsmall, the numerical threshold hthr, the gauge-ratio cap hgauge, and the four named inputs.

The obligation

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureInteriorBesovEnvelopeInput_proved (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ClosureInteriorBesovEnvelopeInput d

Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput, proved.

Conditional on the standing 2 <= d only, and otherwise proved from the ingredients listed in the module docstring.