CombineFiniteCarrierTransport

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

Carrier transport for the finite-corridor two-plus-eight estimate

The quantitative finite-corridor estimate of CombineFiniteVariance is stated at the same-cutoff relative-normalized law Cutoff.relativeNormalizedCutoffLaw M L, which is exactly the spatial pushforward Measure.map (dilateReg (-(L + c))) (Cutoff.coefficientCutoffLaw M L) of the genuine coefficient cutoff law (cutoffRelativeNormalizationShift d = c is dimension-only). This module supplies that missing half and chains it with the proved corridor estimate.

Under the dilation the relative cube at scale n - (L + c) corresponds to the physical cube at scale n, which is the scale correspondence already used for the annealed comparator (annealedBlockMatrixAtScale_relativeNormalizedCutoffLaw). The deterministic centering matrix is carried through unchanged: all transport statements below are stated for an arbitrary deterministic C : BlockMat d, so no centering convention is smuggled in. The identification of that centering with the genuine law's annealed block matrix at the physical scale n is recorded separately in annealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center and, in the scalar form actually carried by the corridor estimate, in scalarAnnealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center_eq.

Main results

• starredFluctuationOperatorNormSq_dilateReg_of_aelocallyUniformlyElliptic
• integral_starredFluctuationOperatorNormSq_relativeNormalizedCutoffLaw
• integral_starredFluctuationOperatorNormSq_relativeNormalizedCutoffLaw_originCube
• scalarAnnealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center_eq
• exists_coefficientCutoff_finiteCorridor_starredFluctuationVariance_bound

The dilation as a measurable equivalence

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.dilateRegEquiv {d : ℕ} (k : ℤ) : HCPolySupport.RegCoeffField d ≃ᵐ HCPolySupport.RegCoeffField d

Triadic dilation of the coefficient carrier, packaged as a measurable equivalence; its inverse is the opposite dilation.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.dilateRegEquiv k = Algsuperdiff.Section3.Cutoff.dilateRegMeasurableEquiv k

Pointwise transport of the starred carriers

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix_dilateReg_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : starredFluctuationMatrix B C (HCPolySupport.cubeSet Q) (HCPolySupport.dilateReg k a) = starredFluctuationMatrix B C (HCPolySupport.cubeSet (HCPolySupport.Book.Ch02.dilateCube (-k) Q)) a

The starred fluctuation matrix on a cube, evaluated at a dilated coefficient field, is the starred fluctuation matrix on the correspondingly dilated cube evaluated at the original field. The deterministic centering is untouched.

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationOperatorNormSq_dilateReg_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet Q) (HCPolySupport.dilateReg k a) = starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet (HCPolySupport.Book.Ch02.dilateCube (-k) Q)) a

Squared operator norm form of starredFluctuationMatrix_dilateReg_of_aelocallyUniformlyElliptic.

Integral transport to the genuine coefficient cutoff law

theorem Algsuperdiff.Section3.Provider.Homogenization.integral_starredFluctuationOperatorNormSq_relativeNormalizedCutoffLaw {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet Q) a ∂Cutoff.relativeNormalizedCutoffLaw M L = ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet (HCPolySupport.Book.Ch02.dilateCube (L + ↑(Cutoff.cutoffRelativeNormalizationShift d)) Q)) a ∂Cutoff.coefficientCutoffLaw M L

Transport of the starred fluctuation integral itself from the relative-normalized law to the genuine coefficient cutoff law.

theorem Algsuperdiff.Section3.Provider.Homogenization.integral_starredFluctuationOperatorNormSq_relativeNormalizedCutoffLaw_originCube {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) : ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet (HCPolySupport.originCube d (n - (L + ↑(Cutoff.cutoffRelativeNormalizationShift d))))) a ∂Cutoff.relativeNormalizedCutoffLaw M L = ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a ∂Cutoff.coefficientCutoffLaw M L

The relative observation cube at relative scale n - (L + c) is the physical observation cube at scale n: the starred fluctuation itself.

theorem Algsuperdiff.Section3.Provider.Homogenization.annealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.relativeNormalizedCutoffLaw M L) (n - L - ↑(Cutoff.cutoffRelativeNormalizationShift d)) = HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n

Scale correspondence of the deterministic centering. The annealed block matrix of the relative law at relative centering scale n - L - c is the annealed block matrix of the genuine coefficient cutoff law at the physical scale n; this identifies the centering carried through the transport statements above.

theorem Algsuperdiff.Section3.Provider.Homogenization.scalarAnnealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center_eq {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) : HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale ⋯ ⋯ (n - L - ↑(Cutoff.cutoffRelativeNormalizationShift d)) = HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n

Consumer-facing reading of the deterministic centering carried by exists_coefficientCutoff_finiteCorridor_starredFluctuationVariance_bound: it is exactly the G coefficient cutoff law's annealed block matrix at the physical scale n.

The genuine-law finite-corridor variance bound

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_coefficientCutoff_finiteCorridor_starredFluctuationVariance_bound (d : ℕ) : ∃ (Chom : ℝ) (Cvar : ℝ), 64 ≤ Chom ∧ 2 * (↑(Cutoff.cutoffRelativeNormalizationShift d) + 1) ≤ Chom ∧ 1 ≤ Cvar ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∀ (L : ℤ), ↑L ≤ ↑m - Chom * |Real.log epsilon| → ∀ n ∈ Set.Icc L m, have hd := ⋯; have c := ↑(Cutoff.cutoffRelativeNormalizationShift d); have hP := ⋯; have hStruct := ⋯; have center := n - L - c; have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M L)); have Cn := HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center; have delta := ↑E ^ 2 * M.gamma + Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)); have decay := Real.rpow 3 (-↑d * ↑(n - L).toNat); ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B Cn (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a ∂Cutoff.coefficientCutoffLaw M L ≤ Cvar * delta * (delta + decay)

Uniform quantitative literal two-plus-eight control of the starred fluctuation itself, at the G coefficient cutoff law and the physical observation cube □_n, along the whole integer corridor L ≤ n ≤ m above the cutoff.

This is the carrier-transported form of exists_relativeCutoff_finiteCorridor_fluctuationVariance_bound (CombineFiniteVariance): the constants, the premise set, the deterministic centering and the decay 3^(-d(n-L)) are unchanged; only the law and the observation cube are moved across the dilation Cutoff.relativeNormalizedCutoffLaw M L = Measure.map (dilateReg (-(L + c))) (Cutoff.coefficientCutoffLaw M L). The deterministic centering Cn is the relative law's scalar annealed block matrix at relative scale n - L - c; by scalarAnnealedBlockMatrixAtScale_relativeNormalizedCutoffLaw_center_eq this is, for every integer n, the genuine cutoff law's annealed block matrix Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n at the physical scale n. This is a local Provider theorem and makes no source-node status claim.