Step5SampDef

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

hsampDef, and Closure.ClosureStep5Input

Closure.Step5Input.closureStep5Input_of_sampDef reduces Closure.ClosureStep5Input to the single binder hsampDef: the sample integrability of Closure.JunctionDischargeStepFiveDisplay.step5CrossDefect at the closure's own Dirichlet family. This module discharges that binder inside the regime in which it is read and produces Closure.ClosureStep5Input.

The two halves of hsampDef

• Measurability is Closure.Step5SampDefMeasurable: the cube average of the product e . ((k_{n+h} - k_n) grad w_D) is a Caratheodory function of the corrector's L^2 class, hence measurable in the sample.
• Domination is the manuscript's own per-cube step: Closure.Step5DefectGauge.step5CrossDefect_le_meshOscillationCell is one sided, and the defect is linear in the direction, so reading it at -e (whose norm is the same, and whose right-hand side is unchanged) gives the two-sided bound

    |defect_R| <= Cdef * ( osc_R * ( 3^nmesh * G_h(z_R) ) ) .
  

  Both factors are L^4 in the sample on the closure's grid --- the oscillation cell by Closure.Step5InputOscillation.exists_gamma0_step5OscillationLegs, the re-sited gauge by Closure.Step5Basket.memLp_four_step5Gauge --- so their product is integrable by Cauchy--Schwarz and the defect is integrable by domination.

Why the regime is entered first

closureStep5Input_of_sampDef carries hsampDef for all parameters, whereas the two L^4 legs above exist only where the manuscript proves them: at a unit direction, at a positive shell width, and on a mesh grid of scale at most n (the per-cube step needs R.scale <= n). This module therefore reproduces the assembly of closureStep5Input_of_sampDef --- the same nine discharged legs, the same produced constants = max (max (step5GateConst d) closureRegimeConst) ((3/2) gamma0^{-1})andFend = step5ShellMomentConst d * --- and supplies hsampDef at the point where the grid, the direction and the shell width are the closure's own. No hypothesis of the assembly is changed, weakened or added.

References

• ABK26, l.approximate.recurrence.formula, Step 5; e.nablaw.oscillations; e.lower.bound.oscillations.

The defect is odd in the direction

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecNormSq_neg {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (-e) = HCPolySupport.vecNormSq e

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecNorm_neg {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (-e) = HCPolySupport.Book.Ch02.vecNorm e

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeAverage_neg {d : ℕ} (R : HCPolySupport.TriadicCube d) (f : HCPolySupport.Vec d → ℝ) : (HCPolySupport.cubeAverage R fun (x : HCPolySupport.Vec d) => -f x) = -HCPolySupport.cubeAverage R f

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.step5CrossDefect_neg_direction {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : step5CrossDefect R omega n m (-e) u = -step5CrossDefect R omega n m e u

The per-cube cross defect is linear in the direction; in particular reading it at -e flips its sign.

The two-sided per-cube step

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.abs_step5CrossDefect_le_meshOscillationCell {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (n m : ℤ) (hsc : R.scale ≤ n) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e ≤ 1) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure R)) : |step5CrossDefect R omega n m e u| ≤ step5CrossDefectConst d * (meshOscillationCell R.scale u R * (3 ^ ↑R.scale * shellDerivNormSum n m (HCPolySupport.triadicCubeShift R) omega))

The two-sided form of the per-cube step. The proved bound is one sided; the defect is odd in the direction and its bound does not see the direction, so reading the proved bound at -e closes the other side.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.abs_step5CrossDefect_le_step5Gauge {d : ℕ} {K : ℤ} {j : ℕ} {nmesh n m : ℤ} (hmesh : K - ↑j = nmesh) (hsc : nmesh ≤ n) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e ≤ 1) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) j) (omega : Cutoff.ShellSeq d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure R)) : |step5CrossDefect R omega n m e u| ≤ step5CrossDefectConst d * (meshOscillationCell nmesh u R * (3 ^ ↑nmesh * shellDerivNormSum n m (HCPolySupport.triadicCubeShift R) omega))

The two-sided per-cube step on the closure's own mesh grid.

Domination by a product of two L^4 factors

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_of_abs_le_const_mul_memLp_four {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] {f a b : Omega → ℝ} (c : ℝ) (hf : MeasureTheory.AEStronglyMeasurable f mu) (ha : MeasureTheory.MemLp a 4 mu) (hb : MeasureTheory.MemLp b 4 mu) (hbound : ∀ (omega : Omega), |f omega| ≤ c * (a omega * b omega)) : MeasureTheory.Integrable f mu

A random variable dominated by a constant multiple of a product of two nonnegative L^4 factors is integrable: the product is L^1 by Cauchy--Schwarz.

Closure.ClosureStep5Input

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureStep5Input (d : ℕ) [NeZero d] : ClosureStep5Input d

Closure.ClosureStep5Input, produced.

Every leg of the Step-5 endpoint at the closure's own corrector families is proved: the nine legs of Closure.Step5Input.closureStep5Input_of_sampDef and, here, the tenth, hsampDef. The produced constants are the same as that theorem's, C5 = max (max (step5GateConst d) closureRegimeConst) ((3/2) gamma0^{-1}) and Fend = step5ShellMomentConst d * C2.

Proved from the ingredients listed in the module docstring.