SuperdiffusivityComponentsModel

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

Model data for the annealed superdiffusivity components

This module supplies the six non-quenched fields of SuperdiffusivityV2Components from the scale family and the generator-renormalization family. The selected random variables are exactly

  EB (confinementScale S L omega) omega,
  3 ^ confinementScale S L omega,

where L = K sqrt(|log gamma|) intrinsicScale. The final constructor keeps the two quenched inequalities as separately named inputs; they are the outputs of QuenchedMomentsComposer.lean.

The common constant envelope

noncomputable def Algsuperdiff.Section5.Provider.superdiffusivityV2ComponentConstant (CS Cren K : ℝ) : ℝ

A common constant for the selected renormalization-error moments, the selected confinement-radius moment, and the loss in the admissible exponent range.

Equations

• Algsuperdiff.Section5.Provider.superdiffusivityV2ComponentConstant CS Cren K = max 1 (max (8 * Cren) (max (81 * √2 * CS * Cren) (2187 / 2 * CS ^ 2 * K)))

theorem Algsuperdiff.Section5.Provider.eight_mul_le_superdiffusivityV2ComponentConstant (CS Cren K : ℝ) : 8 * Cren ≤ superdiffusivityV2ComponentConstant CS Cren K

theorem Algsuperdiff.Section5.Provider.errorCoefficient_le_superdiffusivityV2ComponentConstant (CS Cren K : ℝ) : 81 * √2 * CS * Cren ≤ superdiffusivityV2ComponentConstant CS Cren K

theorem Algsuperdiff.Section5.Provider.radiusCoefficient_le_superdiffusivityV2ComponentConstant (CS Cren K : ℝ) : 2187 / 2 * CS ^ 2 * K ≤ superdiffusivityV2ComponentConstant CS Cren K

Measurability and transport to the full-sample carrier

Positivity and measurability

theorem Algsuperdiff.Section5.Provider.selectedRenormalizationError_nonneg {d : ℕ} (M : Section3.ABKModel d) (S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (L : ℝ) (hEBnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB n omega) (omega : Field.FullSample d M.gamma) : 0 ≤ EB (Support.confinementScale S L ↑omega) ↑omega

The selected renormalization error is nonnegative on the full-sample carrier.

theorem Algsuperdiff.Section5.Provider.selectedConfinementRadius_nonneg {d : ℕ} (M : Section3.ABKModel d) (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (L : ℝ) (omega : Field.FullSample d M.gamma) : 0 ≤ 3 ^ Support.confinementScale S L ↑omega

The selected triadic confinement radius is nonnegative.

theorem Algsuperdiff.Section5.Provider.selectedRenormalizationError_aemeasurable {d : ℕ} (M : Section3.ABKModel d) (S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (L : ℝ) (hSmeas : ∀ (n : ℤ), Measurable (S n)) (hEBmeas : ∀ (n : ℤ), Measurable (EB n)) : AEMeasurable (fun (omega : Field.FullSample d M.gamma) => EB (Support.confinementScale S L ↑omega) ↑omega) ↑(Field.fullSampleLaw M)

The selected renormalization error is almost everywhere measurable on the full-sample carrier.

theorem Algsuperdiff.Section5.Provider.selectedConfinementRadius_aemeasurable {d : ℕ} (M : Section3.ABKModel d) (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (L : ℝ) (hSmeas : ∀ (n : ℤ), Measurable (S n)) : AEMeasurable (fun (omega : Field.FullSample d M.gamma) => 3 ^ Support.confinementScale S L ↑omega) ↑(Field.fullSampleLaw M)

The selected triadic confinement radius is almost everywhere measurable on the full-sample carrier.

Exponent and amplitude arithmetic

The selected moments on the full-sample carrier

theorem Algsuperdiff.Section5.Provider.selectedRenormalizationError_moment_two {d : ℕ} (M : Section3.ABKModel d) {cstar t p C0 CS Cren K : ℝ} (hcstar : 0 < cstar) (ht : 0 < t) (hp : 1 ≤ p) (hCS : 1 ≤ CS) (hCren : 0 < Cren) (hK : 1 ≤ K) (hC0 : superdiffusivityV2ComponentConstant CS Cren K ≤ C0) (hrange : p ≤ C0⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) {S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hSmeas : ∀ (n : ℤ), Measurable (S n)) (hSnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) (hSmom4 : ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (4 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (4 * p)) (hEBmeas : ∀ (n : ℤ), Measurable (EB n)) (hEBmom : ∀ (n : ℤ) (q : ℝ), 1 ≤ q → q ≤ Cren⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB n omega) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Cren * (√q + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ q) : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (EB (Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ↑omega) ^ (2 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ (2 * p)

The 2p moment of the selected renormalization error, in exactly the proposition used by SuperdiffusivityV2Components.

theorem Algsuperdiff.Section5.Provider.selectedRenormalizationError_moment_four {d : ℕ} (M : Section3.ABKModel d) {cstar t p C0 CS Cren K : ℝ} (hcstar : 0 < cstar) (ht : 0 < t) (hp : 1 ≤ p) (hCS : 1 ≤ CS) (hCren : 0 < Cren) (hK : 1 ≤ K) (hC0 : superdiffusivityV2ComponentConstant CS Cren K ≤ C0) (hrange : p ≤ C0⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) {S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hSmeas : ∀ (n : ℤ), Measurable (S n)) (hSnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) (hSmom8 : ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (8 * p)) (hEBmeas : ∀ (n : ℤ), Measurable (EB n)) (hEBmom : ∀ (n : ℤ) (q : ℝ), 1 ≤ q → q ≤ Cren⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB n omega) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Cren * (√q + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ q) : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (EB (Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ↑omega) ^ (4 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ (4 * p)

The 4p moment of the selected renormalization error, in exactly the proposition used by SuperdiffusivityV2Components.

theorem Algsuperdiff.Section5.Provider.selectedConfinementRadius_moment_four {d : ℕ} (M : Section3.ABKModel d) {cstar t p C0 CS K Cren : ℝ} (hcstar : 0 < cstar) (ht : 0 < t) (hp : 1 ≤ p) (hCS : 1 ≤ CS) (hK : 1 ≤ K) (hC0 : superdiffusivityV2ComponentConstant CS Cren K ≤ C0) {S : ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hSmeas : ∀ (n : ℤ), Measurable (S n)) (hSnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) (hSmom8 : ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (8 * p)) : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (3 ^ Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ^ (4 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ^ (4 * p)

The 4p moment of the selected triadic confinement radius, in exactly the proposition used by SuperdiffusivityV2Components.

Construction once the two quenched fields are supplied

noncomputable def Algsuperdiff.Section5.Provider.superdiffusivityV2ComponentsOfQuenched {d : ℕ} (M : Section3.ABKModel d) [NeZero d] {cstar t p C0 CS Cren K : ℝ} (hcstar : 0 < cstar) (ht : 0 < t) (hp : 1 ≤ p) (hCS : 1 ≤ CS) (hCren : 0 < Cren) (hK : 1 ≤ K) (hC0 : superdiffusivityV2ComponentConstant CS Cren K ≤ C0) (hrange : p ≤ C0⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) {S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hSmeas : ∀ (n : ℤ), Measurable (S n)) (hSnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) (hSmom4 : ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (4 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (4 * p)) (hSmom8 : ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (8 * p)) (hEBnn : ∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB n omega) (hEBmeas : ∀ (n : ℤ), Measurable (EB n)) (hEBmom : ∀ (n : ℤ) (q : ℝ), 1 ≤ q → q ≤ Cren⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB n omega) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Cren * (√q + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ q) (hsecond : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), |∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - 2 * ↑d * Support.intrinsicScale M.nu cstar M.gamma t ^ 2| ≤ C0 * (EB (Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ↑omega + √M.gamma * |Real.log M.gamma|) * (3 ^ Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ^ 2) (hmeanSq : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), HCPolySupport.vecNormSq (∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) ≤ C0 * (EB (Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ↑omega ^ 2 + M.gamma ^ 80) * (3 ^ Support.confinementScale S (K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ↑omega) ^ 2) : SuperdiffusivityV2Components M cstar t p C0

Build the full component structure from the scale and renormalization families once the two quenched inequalities have been supplied by the quenched composer.

Equations

• One or more equations did not get rendered due to their size.