Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section51.ShiftedP4

Coarse-graining support: Support.Book.Ch05.Theorems.Section51.ShiftedP4 #

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

Shifted (P4) data for the main theorem #

The Section 5.5 localization produces smallness for the 2β-shifted moment quantity. Since the Lean value of β is chosen with enough slack, these shifted exponents still define valid (P4) data. This file packages that renaming of exponents.

source
theorem HCPolySupport.Book.Ch05.Section51.section53CoarseFluctuationBetaParams_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
0 < Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params
source
theorem HCPolySupport.Book.Ch05.Section51.twoBetaShiftedParams_sum_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
params.sUpper + 2 * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params + (params.sLower + 2 * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params) < 1
source
theorem HCPolySupport.Book.Ch05.Section51.twoBetaShiftedParams_sUpper_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
params.sUpper + 2 * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params < 1
source
theorem HCPolySupport.Book.Ch05.Section51.twoBetaShiftedParams_sLower_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
params.sLower + 2 * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params < 1
source
noncomputable def HCPolySupport.Book.Ch05.Section51.twoBetaShiftedParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
QuantitativeCoarseGrainedEllipticityParams d

Parameter-only (P4) data with both exponents shifted by 2β.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch05.Section51.twoBetaShiftedP4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) :
    QuantitativeCoarseGrainedEllipticity P

    Law-specific (P4) data with both exponents shifted by 2β.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.Book.Ch05.Section51.twoBetaShiftedP4_params {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      (twoBetaShiftedP4 hP hStruct hP4).params = twoBetaShiftedParams hP4.params
      source
      theorem HCPolySupport.Book.Ch05.Section51.widetildeThetaAtScale_twoBetaShiftedP4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (n : ℤ) :
      widetildeThetaAtScale P n (twoBetaShiftedP4 hP hStruct hP4) = Section55.shiftedWidetildeThetaAtScale P n hP4 (2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4)
      source
      theorem HCPolySupport.Book.Ch05.Section51.widetildeThetaAtScale_zero_scaleNormalized_twoBetaShiftedP4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k : ℕ) :
      widetildeThetaAtScale (Ch04.restrictionScaleNormalizedLaw k P) 0 (twoBetaShiftedP4 ⋯ ⋯ (hP4.scaleNormalized hP hStruct k)) = Section55.shiftedWidetildeThetaAtScale P (↑k) hP4 (2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4)