CGBoundSpecialization #

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

ABK26's `e.basecase.tightbound` #

ABK26, specializes the deterministic coarse-graining ellipticity chain e.CG.bounds.1 to the infrared cutoff coefficient a_m = nu I + k_m:

nu Id <= s_{m,*}(cu_l) <= s_m(cu_l) <= b_m(cu_l) <= nu (1 + nu^{-2} ||k_m||^2_{L2bar(cu_l)}) Id,

for every m, l in Z and every sample.

The specialization is exact, not an estimate. The symmetric part of the cutoff coefficient is identically nu I (Algsuperdiff.Section3.Cutoff.symmPart_coefficientCutoff), so the harmonic mean on the left of e.CG.bounds.1 is nu Id, and the averaged correction on the right is nu Id + nu^{-1} (fint_{cu_l} k_m^t k_m) . Only the last step, k^t k <= ||k||_F^2 Id, is an inequality.

The Loewner order is CoarseGraining's Homogenization.MatLoewnerLE, the coarse matrices are CoarseGraining's Chapter 2 objects on the Chapter 2 cube domain, and the volume normalized L^2 mass of k_m is Ch02.average (Ch02.cubeDomain (originCube d l)) (fun x => Ch02.matrixFrobeniusNormSq (cutoff m omega x)), the same expression whose expectation is computed by Algsuperdiff.Section3.Provider.Stream.integral_average_frobeniusMass_cutoff.

Main results #

skewPart_coefficientCutoff, inv_symmPart_coefficientCutoff
averagedSymmPartInv_coefficientCutoff, averagedSymmPartPlusCorrection_coefficientCutoff
matLoewnerLE_nu_smul_one_sigmaStarCoarse_coefficientCutoff
matLoewnerLE_bCoarse_coefficientCutoff
matLoewnerLE_nu_smul_one_bCoarse_coefficientCutoff: the composed lower leg of e.basecase.tightbound, placing nu Id below b_m(cu_l).

References #

ABK26, e.basecase.tightbound.
ABK26, e.CG.bounds.1.

Pointwise algebra of the cutoff coefficient #

source

theorem Algsuperdiff.Section3.Provider.Base.vecDot_matVecMul_smul_one {d : ℕ} (c : ℝ) (xi : HCPolySupport.Vec d) :

HCPolySupport.vecDot xi (HCPolySupport.matVecMul (c • 1) xi) = c * HCPolySupport.vecNormSq xi

The quadratic form of a scalar matrix.

source

theorem Algsuperdiff.Section3.Provider.Base.skewPart_coefficientCutoff {d : ℕ} (nu : ℝ) (m : ℤ) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) :

HCPolySupport.skewPart ((Cutoff.coefficientCutoff nu m omega).toFun x) = (Cutoff.cutoff m omega).toFun x

The skew part of the cutoff coefficient is the stream matrix k_m. This is a pointwise identity: a_m = nu I + k_m with k_m antisymmetric.

source

theorem Algsuperdiff.Section3.Provider.Base.inv_symmPart_coefficientCutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) :

(HCPolySupport.symmPart ((Cutoff.coefficientCutoff M.nu m omega).toFun x))⁻¹ = M.nu⁻¹ • 1

The pointwise inverse symmetric part of the cutoff coefficient is nu^{-1} I, exactly.

source

theorem Algsuperdiff.Section3.Provider.Base.symmPartPlusCorrection_coefficientCutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) :

HCPolySupport.symmPart ((Cutoff.coefficientCutoff M.nu m omega).toFun x) + HCPolySupport.matTranspose (HCPolySupport.skewPart ((Cutoff.coefficientCutoff M.nu m omega).toFun x)) * (HCPolySupport.symmPart ((Cutoff.coefficientCutoff M.nu m omega).toFun x))⁻¹ * HCPolySupport.skewPart ((Cutoff.coefficientCutoff M.nu m omega).toFun x) = M.nu • 1 + M.nu⁻¹ • (HCPolySupport.matTranspose ((Cutoff.cutoff m omega).toFun x) * (Cutoff.cutoff m omega).toFun x)

The pointwise integrand of the right-hand side of e.CG.bounds.1, for the cutoff coefficient: symm + skew^t symm^{-1} skew = nu I + nu^{-1} k_m^t k_m.

source

theorem Algsuperdiff.Section3.Provider.Base.vecDot_matVecMul_correction {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (x xi : HCPolySupport.Vec d) :

HCPolySupport.vecDot xi (HCPolySupport.matVecMul (M.nu • 1 + M.nu⁻¹ • (HCPolySupport.matTranspose ((Cutoff.cutoff m omega).toFun x) * (Cutoff.cutoff m omega).toFun x)) xi) = M.nu * HCPolySupport.vecNormSq xi + M.nu⁻¹ * HCPolySupport.vecNormSq (HCPolySupport.matVecMul ((Cutoff.cutoff m omega).toFun x) xi)

The quadratic form of the pointwise correction matrix.

The two averaged coefficient matrices of `e.CG.bounds.1` #

source

theorem Algsuperdiff.Section3.Provider.Base.averagedSymmPartInv_coefficientCutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) :

HCPolySupport.Book.Ch02.averagedSymmPartInv (HCPolySupport.Book.Ch02.cubeDomain Q) (Cutoff.coefficientCutoffCoeffOn M m omega Q) = M.nu⁻¹ • 1

The harmonic-mean matrix of the cutoff coefficient is nu^{-1} I on every triadic cube.

source

theorem Algsuperdiff.Section3.Provider.Base.averagedSymmPartPlusCorrection_coefficientCutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) :

HCPolySupport.Book.Ch02.averagedSymmPartPlusCorrection (HCPolySupport.Book.Ch02.cubeDomain Q) (Cutoff.coefficientCutoffCoeffOn M m omega Q) = HCPolySupport.Book.Ch02.averageMat (HCPolySupport.Book.Ch02.cubeDomain Q) fun (x : HCPolySupport.Vec d) => M.nu • 1 + M.nu⁻¹ • (HCPolySupport.matTranspose ((Cutoff.cutoff m omega).toFun x) * (Cutoff.cutoff m omega).toFun x)

The averaged upper coefficient matrix of the cutoff coefficient.

Continuity and integrability on an origin cube #

source

theorem Algsuperdiff.Section3.Provider.Base.integrableOn_frobeniusMass_cutoff {d : ℕ} (ell m : ℤ) (omega : Cutoff.CutoffSample d) :

MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x)) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) MeasureTheory.volume

The Frobenius mass of k_m is integrable on every origin cube: it is continuous and bounded there by the proved local control of the cutoff.

The two ends of the specialized chain #

source

theorem Algsuperdiff.Section3.Provider.Base.matLoewnerLE_nu_smul_one_sigmaStarCoarse_coefficientCutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) :

HCPolySupport.MatLoewnerLE (M.nu • 1) (HCPolySupport.Book.Ch02.sigmaStarCoarse (HCPolySupport.Book.Ch02.cubeDomain Q) (Cutoff.coefficientCutoffCoeffOn M m omega Q))

ABK26. The left-hand leg of e.basecase.tightbound: the harmonic mean of the cutoff coefficient is exactly nu Id, so the coarse starred matrix dominates nu Id.

source