Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.SplitFoldIntegrability

SplitFoldIntegrability #

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

Conjuncts (1) and (2) of SplitScaleObligations, with no analytic binder #

ABK26, l.approximate.recurrence.formula, Steps 1--3, e.recurrence.params.

Closure.SplitObligations.splitScaleObligations_integrability_of_regime produces the two integrability conjuncts of Closure.SplitProducerFold.SplitScaleObligations from one analytic binder hmom. Closure.SplitFoldCellMoments proves both moments; this module chains them and re-runs the same assembly inside the regime, so that the export

  splitScaleObligations_integrability_closureFamilies

carries exactly Closure.ClosureRegime at the produced threshold and the two direction bounds --- no hmom, no measurability, no smallness.

After this module the residual of SplitScaleObligations at the closure's families is exactly conjunct (3),

  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 ,

which is Step 2 of the manuscript and is not proved here.

Scope #

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References #

The two cell-energy moments, produced #

source
theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_closureCellMoments (d : ℕ) [NeZero d] (hd : 2 ≤ d) :
∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (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⁻¹ → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (K : ℕ), 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → n + ↑h ≤ ↑K → ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshCellBackgroundPotentialEnergy M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2) ↑(Cutoff.cutoffSampleLaw M) ∧ MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshCellBackgroundFluxEnergy M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega) ↑(Cutoff.cutoffSampleLaw M)

hmom of Closure.SplitObligations.splitScaleObligations_integrability_of_regime, as a theorem, at the closure's own corrector families and in the parameter range of e.recurrence.params.

For every mesoscopic cell of the closure mesh below a sufficiently large localization cube: the second sample moment of the Step-2 background's normalized potential cell energy, and the first sample moment of its flux cell energy.

Conjuncts (1) and (2), at the closure families, inside the regime #

source
theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.splitScaleObligations_integrability_closureFamilies (d : ℕ) [NeZero d] (hd : 2 ≤ d) :
∃ (Csplit : ℝ), 0 < Csplit ∧ ∀ (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 Csplit M n h Ec → ∀ᶠ (K : ℕ) in Filter.atTop, (∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M (n + ↑h) R (principalPz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)) omega) ↑(Cutoff.cutoffSampleLaw M)) ∧ ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega)) ↑(Cutoff.cutoffSampleLaw M)

Obligations (1) and (2) of Closure.SplitProducerFold.SplitScaleObligations, produced with no analytic binder.

exactly on Closure.ClosureRegime at the produced threshold and the two direction bounds |e| <= 1, |e'| <= 1. This is Closure.SplitObligations.splitScaleObligations_integrability_of_regime with its binder hmom discharged by exists_gamma0_closureCellMoments.

What is left of SplitScaleObligations #

source
theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.splitScaleObligations_of_fluctuation {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) (hprin : ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M (n + ↑h) R (principalPz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)) omega) ↑(Cutoff.cutoffSampleLaw M)) (hbg : ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega)) ↑(Cutoff.cutoffSampleLaw M)) (hfluct : 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) :
SplitScaleObligations M n h K e e'

SplitScaleObligations from the two produced integrabilities and the cgamma^10 estimate.

A repackaging with no content: after splitScaleObligations_integrability_closureFamilies the residual of the three obligations is exactly conjunct (3), Step 2 itself. Anchor-free.

ClosureSplitInput, one estimate away #

source
theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecNorm_zero_le_one_fold {d : ℕ} :
HCPolySupport.Book.Ch02.vecNorm 0 ≤ 1
source
theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureSplitInput_of_gammaTenBound (d : ℕ) [NeZero d] (hd : 2 ≤ d) {Cfl : ℝ} (hfluct : ∀ (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) :
ClosureSplitInput d

Closure.ClosureFinal.ClosureSplitInput from the cgamma^10 estimate alone.

Every other ingredient of the finite-grid half of Steps 1--3 at the closure's own corrector families is discharged: the two integrability conjuncts by splitScaleObligations_integrability_closureFamilies, and the whole Step-1--3 assembly by Closure.SplitProducerFold.closureSplitInput_of_obligations. What is left is verbatim Step 2 of the manuscript, at both direction pairs.

exactly on hfluct; the threshold is the maximum of the produced one and the caller's Cfl.