SplitObligationsQuadratic

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

The per-cube coarse quadratic upper bound at the genuine cutoff

ABK26, l.approximate.recurrence.formula, Steps 1--2; the coarse-graining chain e.CG.bounds.2.

What this module supplies

Both surviving integrability obligations of Closure.SplitProducerFold.SplitScaleObligations need one and the same pathwise dominator: an upper bound for a doubled coarse quadratic form by an explicit multiple of the two squared component lengths, whose random constant is the realised upper ellipticity constant Cutoff.coefficientCutoffCubeEllipticityUpper of the cell. This module proves it.

The route is the proved right leg of e.CG.bounds.2:

  X . bfA(U; a) X  <=  X . ( fint_U bfA(x) dx ) X
                    =  fint_U  X . bfA(x) X  dx
                    <=  ( Lam + 2 lam^{-1} Lam^2 ) |X_1|^2 + 2 lam^{-1} |X_2|^2 ,

the first step being Provider.Block.coarseBlockMatrix_blockMatLoewnerLE_averagedBlockMatrix, the second Provider.Block.average_blockVecDot_blockMatVecMul_blockMatrixField, and the third CoarseGraining's pointwise Homogenization.blockMatrixOfCoeff_quadratic_plainUpperBound_of_isEllipticMatrix under CoeffOn.aeElliptic.

At the genuine cutoff family the two ellipticity constants of the cell are lam = M.nu and Lam = Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R, both definitionally (Cutoff.coefficientCutoffCoeffOn), so switchCubeEnergy_le_ellipticityUpper reads the bound directly at the Step-3 switch energy.

Binders

Only the typing binders. Every statement below is unconditional: no smallness, moment, measurability or selection proposition occurs.

Scope

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

References

• ABK26, e.CG.bounds.2, l.approximate.recurrence.formula, Steps 1--3, the switch display.

Normalized averages against a constant

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.volume_domain_toReal_pos {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) : 0 < (MeasureTheory.volume U.carrier).toReal

A Chapter 2 domain has positive finite volume.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.average_le_of_ae_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {f : HCPolySupport.Vec d → ℝ} {c : ℝ} (hf : MeasureTheory.Integrable f (HCPolySupport.volumeMeasureOn U.carrier)) (hle : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U.carrier, f x ≤ c) : HCPolySupport.Book.Ch02.average U f ≤ c

The normalized average of an integrable function almost everywhere below a constant is below that constant.

The coarse quadratic upper bound

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.blockVecDot_coarseBlockMatrix_le_plainUpperBound {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) X) ≤ (a.Lam + 2 * a.lam⁻¹ * a.Lam ^ 2) * HCPolySupport.vecNormSq X.1 + 2 * a.lam⁻¹ * HCPolySupport.vecNormSq X.2

The doubled coarse quadratic form is bounded by the plain elliptic upper bound of its own carrier.

e.CG.bounds.2's right leg followed by CoarseGraining's pointwise doubled upper bound. Unconditional: the two constants are the ones the CoeffOn carrier itself records.

The bound at the genuine cutoff cell

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.switchCubeEnergy_le_ellipticityUpper {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (X : HCPolySupport.BlockVec d) (omega : Cutoff.CutoffSample d) : switchCubeEnergy M m R X omega ≤ (Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R + 2 * M.nu⁻¹ * Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R ^ 2) * HCPolySupport.vecNormSq X.1 + 2 * M.nu⁻¹ * HCPolySupport.vecNormSq X.2

The Step-3 switch energy, bounded by the realised upper ellipticity constant of its own cell.

(meshCellCoeff M m R omega).lam = M.nu and .Lam = Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R hold definitionally, so the previous bound reads verbatim at the switch energy. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.coefficientCutoffCubeEllipticityUpper_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) (R : HCPolySupport.TriadicCube d) : 0 ≤ Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R

The realised upper ellipticity constant of a cell is nonnegative.