GammaTenStripEnvelopeConst

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

The interior-mesh Besov envelope with the depth input carrying a constant

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

The gap this module fills

The interior route of Closure.GammaTenStripEnvelope reads the per-depth input at exactly cgamma^{16} (1+i) 3^{-i} and returns the grid fourth-moment root at exactly cgamma^{15}, at one and the same cgamma. Both numbers are rigid, and the consumer of the envelope does not read the depth endpoints at those numbers:

• the Besov tower the closure's hosc is stated at is the tower of the gauged bfF_z, which by cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential and ..._flux is a fixed scalar multiple of the tower of the raw field; and
• the flux leg's raw field is neumannFluxField = grad w_N + streamForcing, whose oscillation cell exceeds that of grad w_N by the forcing term of Closure.GammaTenInteriorMinkowski.meshOscillationCell_neumannFluxField_le, again a bounded multiple.

Neither multiple can be pushed through the proved statement: rescaling cgamma moves premise and conclusion together (a factor A >= 1 in the premise costs A^{15/16} in the conclusion, in the wrong direction), so the summation has to be re-run with the constant carried. That is all this module does.

What is proved

• sum_depth_fold_const_le --- the depth fold of the interior route with the constant A carried: a per-depth input 2 (A cgamma^{16} (1+i) 3^{-i})^4 folds to 200 A^4 cgamma^{64}, uniformly in the depth cutoff. The interior route's own fold closes with the numerical step 200 cgamma^{64} <= cgamma^{60}; here that step is omitted rather than applied, so that the caller chooses the budget.
• exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const --- the envelope itself: from a per-depth grid fourth-moment root below A cgamma^{16} (1+i) 3^{-i} and the explicit budget premise 200 A^4 cgamma^{64} <= c^4, a nonnegative sample family B, in L^4 at every cell of interiorMesoCubeGrid d K n outer, dominating every finite-depth positive q = 2 Besov seminorm of U at exponent gammaTenBesovExponent almost surely, whose grid fourth-moment root is below c.

At A = 1, c = cgamma^{15} and 0 < cgamma <= 1/4 the budget premise reduces to 200 cgamma^{64} <= cgamma^{60}, so the interior route's own endpoint is the special case; nothing is weakened.

Binders

Those of the proved composite --- the scale bookkeeping K = n + p, outer + 1 = n + g, g <= p, n <= outer, the boundary gate d 3^{g-p} <= 1/2, the three cellwise typing binders and the per-depth input --- with the quarter bound on cgamma and its positivity removed (the fold no longer performs a numerical step in cgamma) and the two numerical parameters A, c added, the second nonnegative and tied to the first by hbudget. Nothing about the corrector, the coefficient field or the sample space occurs: U is an arbitrary sample-indexed field and mu an arbitrary measure.

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.nablaw.oscillations, e.recurrence.params.

The depth fold with a constant carried

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sum_depth_fold_const_le {gamma A : ℝ} (D : ℕ → ℝ) (hD : ∀ (i : ℕ), D i ≤ 2 * (A * (gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))) ^ 4) (N : ℕ) : ∑ i ∈ Finset.range (N + 1), 2 ^ (i + 1) * Real.rpow 3 (gammaTenBesovExponent * ↑i) ^ 4 * D i ≤ 200 * A ^ 4 * gamma ^ 64

The depth fold of the interior route, with the constant A carried.

The interior route's own fold stops at cgamma^{60}, because it applies its closing numerical step in cgamma; here the fold is left at 200 A^4 cgamma^{64}, which is what a caller with a constant in the per-depth input needs. Unconditional beyond hD.

The composite

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const {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 : Omega → HCPolySupport.Vec d → HCPolySupport.Vec d) {gamma A c : ℝ} (hc0 : 0 ≤ c) (hbudget : 200 * A ^ 4 * gamma ^ 64 ≤ c ^ 4) (hmeascell : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), Measurable fun (w : Omega) => meshOscillationCell (n - ↑i) (U w) R') (hintcell : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.Integrable (fun (w : Omega) => meshOscillationCell (n - ↑i) (U w) R' ^ 4) mu) (hmem2 : ∀ (w : Omega) (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), MeasureTheory.MemLp (U w) 2 (HCPolySupport.normalizedCubeMeasure R')) (hdepth : ∀ (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)))) : ∃ (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 ≤ c ∧ ∀ R ∈ interiorMesoCubeGrid d K n outer, ∀ᵐ (w : Omega) ∂mu, ∀ (N : ℕ), HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N (U w) ≤ B R w

The Besov envelope of Step 2 on the interior mesh, from a depth input carrying a constant.

The mirror of Closure.GammaTenStripEnvelope.exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot whose per-depth input is A cgamma^{16} (1+i) 3^{-i} and whose conclusion is the caller's own budget c, the two being tied by the explicit numerical premise hbudget : 200 A^4 cgamma^{64} <= c^4.

on the scale bookkeeping, the boundary gate hsmall, the budget premise, the three cellwise typing binders and hdepth.