Documentation

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

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

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

Tau-sum absorption for the one-step contraction #

The Section 5.3 coarse-fluctuation estimate contains a beta-weighted sum of additivity defects multiplied by a scalar coefficient combination. At a good scale this term is O(delta * Theta_0), hence also O(sqrt(delta) * Theta_0) in the manuscript range.

source
noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepTauSumAtScale {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.4 beta-weighted additivity-defect sum used in the one-step contraction proof.

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

    The harmless geometric constant for the one-step tau-sum absorption.

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

      The tau-sum constant is nonnegative.

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

      The scalar weight multiplying the tau sum is nonnegative.

      source
      theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepTauSumAtScale_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) :
      oneStepTauSumAtScale hP hStruct hP4 m e ≤ (geometricDiscount (VarianceBoundGoodScale.section54VarianceBeta hP4) 1)⁻¹ * (delta * √(thetaAtScale hP hStruct 0))

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

      source
      theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScalarWeight_mul_tauSum_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) :
      oneStepScalarWeightAtScale hP hStruct m * oneStepTauSumAtScale hP hStruct hP4 m e ≤ oneStepTauSumConst hP4 * delta * thetaAtScale hP hStruct 0

      At a good scale, the scalar-weighted tau sum is O(delta * Theta_0).

      source
      theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScalarWeight_mul_tauSum_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) :
      oneStepScalarWeightAtScale hP hStruct m * oneStepTauSumAtScale hP hStruct hP4 m e ≤ oneStepTauSumConst hP4 * √delta * thetaAtScale hP hStruct 0

      At a good scale, the scalar-weighted tau sum is also O(sqrt(delta) * Theta_0).