Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.OneStepContraction.CoarseRHSPrep

Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.CoarseRHSPrep #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Preparing the Section 5.3 coarse-fluctuation RHS #

This file records the pieces of the final one-step contraction assembly that can be proved before the final Section 5.3 estimate lands. The dependencies on Section 5.3 remain local to the one-step-contraction directory.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationScalarWeightAtScale_eq_oneStepScalarWeightAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℕ) :
Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m = oneStepScalarWeightAtScale hP hStruct m

The scalar weight in the Section 5.3 coarse-fluctuation RHS is exactly the one used by the Section 5.4 one-step contraction proof.

source
noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) :
ℝ

The Section 5.3-beta tau sum, reindexed over natural lower scales.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationTauSumAtScale_zero_eq_oneStepCoarseTauSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) :
    Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 0 m e = oneStepCoarseTauSumAtScale hP hStruct hP4 m e

    At k = 0, the Section 5.3 tau sum is the natural-scale sum used by the one-step proof, with the Section 5.3 beta.

    source
    noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
    ℝ

    The Section 5.3-beta full-block fluctuation sum, reindexed over natural lower scales.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationFullBlockSumAtScale_zero_eq_oneStepCoarseFullBlockSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
      Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 0 m = oneStepCoarseFullBlockSumAtScale hP hStruct hP4 m

      At k = 0, the Section 5.3 full-block fluctuation sum is the natural-scale sum used by the one-step proof, with the Section 5.3 beta.

      source
      theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockSumAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
      0 ≤ oneStepCoarseFullBlockSumAtScale hP hStruct hP4 m

      The reindexed Section 5.3-beta full-block fluctuation sum is nonnegative.

      source
      noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      ℝ

      The harmless geometric constant for the Section 5.3-beta tau sum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
        0 ≤ oneStepCoarseTauSumConst hP4

        The Section 5.3-beta tau-sum constant is nonnegative.

        source
        theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumAtScale_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le : delta ≤ 1 / 2) {m : ℕ} (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (e : Vec d) (he : Ch02.vecNorm e = 1) :
        oneStepCoarseTauSumAtScale hP hStruct hP4 m e ≤ (geometricDiscount (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) 1)⁻¹ * (delta * √(thetaAtScale hP hStruct 0))

        At a good scale, the Section 5.3-beta tau sum is bounded by the geometric tail times delta * sqrt(Theta_0).

        source
        theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationScalarWeight_mul_tauSum_zero_le_delta_theta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le : delta ≤ 1 / 2) {m : ℕ} (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (e : Vec d) (he : Ch02.vecNorm e = 1) :
        Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 0 m e ≤ oneStepCoarseTauSumConst hP4 * delta * thetaAtScale hP hStruct 0

        At a good scale, the scalar-weighted Section 5.3 tau sum at k = 0 is O(delta * Theta_0).

        source
        theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationScalarWeight_mul_tauSum_zero_le_sqrt_delta_theta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le : delta ≤ 1 / 2) {m : ℕ} (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (e : Vec d) (he : Ch02.vecNorm e = 1) :
        Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 0 m e ≤ oneStepCoarseTauSumConst hP4 * √delta * thetaAtScale hP hStruct 0

        At a good scale, the scalar-weighted Section 5.3 tau sum at k = 0 is also O(sqrt(delta) * Theta_0).