Coarse-graining support: Support.Book.Ch05.Theorems.Section55.ShiftedWidetildeTheta

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

Section 5.5 shifted widetildeTheta

This file begins the Lean proof of the shifted localization estimate in Section 5.5. The key point is that the decaying Section 5.2 input is used at the shifted exponents s_1 + beta and s_2 + beta; these exponents are not fed back into (P4) at the next iteration step.

theorem HCPolySupport.Book.Ch05.Section55.rpow_three_neg_beta_nat_le_one {β : ℝ} (hβ : 0 ≤ β) (m : ℕ) : Real.rpow 3 (-β * ↑m) ≤ 1

The beta-decay factor at a natural scale gap is at most one.

noncomputable def HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaAtScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (hP4 : QuantitativeCoarseGrainedEllipticity P) (η : ℝ) : ℝ

The shifted high-moment quantity in Section 5.5.

Equations

• HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaAtScale P n hP4 η = HCPolySupport.Book.Ch04.widetildeThetaAtScale P n (hP4.sUpper + η) (hP4.sLower + η) hP4.xi

noncomputable def HCPolySupport.Book.Ch05.Section55.betaShiftedWidetildeThetaAtScale {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

The beta-specialized shifted high-moment quantity used internally in Section 5.5.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section55.section52TwoExponentMomentBoundCoeff_nonneg {d ξ m : ℕ} {C s r : ℝ} (hC_nonneg : 0 ≤ C) (hs_pos : 0 < s) (hr_lt_one : r < 1) (hd : 2 ≤ d) : 0 ≤ section52TwoExponentMomentBoundCoeff d ξ C s r m

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedWidetildeThetaAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) : betaShiftedWidetildeThetaAtScale (Ch04.restrictionScaleNormalizedLaw k P) (↑m) (hP4.scaleNormalized hP hStruct k) = betaShiftedWidetildeThetaAtScale P (↑(k + m)) hP4

The shifted high-moment quantity is compatible with Ch4 scale normalization.

theorem HCPolySupport.Book.Ch05.Section55.widetildeThetaAtScale_zero_restrictionScaleNormalizedLaw {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 (hP4.scaleNormalized hP hStruct k) = widetildeThetaAtScale P (↑k) hP4

Scale normalization sends scale 0 to the original scale k for the unshifted manuscript widetildeTheta.

theorem HCPolySupport.Book.Ch05.Section55.thetaAtScale_zero_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (k : ℕ) : ⋯.thetaAtScale ⋯ 0 = hP.thetaAtScale hStruct ↑k

Scale normalization sends scale 0 to the original scale k for the structural scalar contrast.

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedWidetildeThetaAtScale_restrictionScaleNormalizedLaw_of_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k n : ℕ} (hkn : k ≤ n) : betaShiftedWidetildeThetaAtScale (Ch04.restrictionScaleNormalizedLaw k P) (↑(n - k)) (hP4.scaleNormalized hP hStruct k) = betaShiftedWidetildeThetaAtScale P (↑n) hP4

Dilation rewrite for the shifted quantity on a window [k,n].

theorem HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaAtScale_le_thetaAtScale_zero_add_error_of_P4_positiveExcess_bounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {rUpper rLower : ℝ} (hrUpper_gt : hP4.sUpper < rUpper) (hrUpper_lt_one : rUpper < 1) (hrLower_gt : hP4.sLower < rLower) (hrLower_lt_one : rLower < 1) (m : ℕ) {coeffUpper coeffLower finalCoeff : ℝ} (hCoeffUpper_nonneg : 0 ≤ coeffUpper) (hCoeffLower_nonneg : 0 ≤ coeffLower) (hUpperExcess : LambdaPositiveExcessMomentAtScale P (↑m) rUpper hP4.xi hP hStruct ≤ coeffUpper * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi) (hLowerExcess : lambdaInvPositiveExcessMomentAtScale P (↑m) rLower hP4.xi hP hStruct ≤ coeffLower * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi) (hCoeff : coeffUpper + coeffLower + coeffUpper * coeffLower ≤ finalCoeff) : Ch04.widetildeThetaAtScale P (↑m) rUpper rLower hP4.xi ≤ thetaAtScale hP hStruct 0 + finalCoeff * widetildeThetaAtScale P 0 hP4

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedWidetildeThetaAtScale_le_thetaAtScale_zero_add_section52TwoExponent_error {d : ℕ} [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ), betaShiftedWidetildeThetaAtScale P (↑m) hP4 ≤ thetaAtScale hP hStruct 0 + (section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sUpper (hP4.sUpper + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m + section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sLower (hP4.sLower + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m + section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sUpper (hP4.sUpper + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m * section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sLower (hP4.sLower + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m) * widetildeThetaAtScale P 0 hP4

theorem HCPolySupport.Book.Ch05.Section55.section52TwoExponentMomentBoundCoeff_upper_beta_shift_le_loss_beta_decay {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {C : ℝ} (hP4 : QuantitativeCoarseGrainedEllipticity P) (hC_nonneg : 0 ≤ C) (m : ℕ) : have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sUpper (hP4.sUpper + β) m ≤ C * section52MomentLossCoeff d hP4.xi hP4.sUpper (hP4.sUpper + β) * Real.rpow 3 (-β * ↑m)

theorem HCPolySupport.Book.Ch05.Section55.section52TwoExponentMomentBoundCoeff_lower_beta_shift_le_loss_beta_decay {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {C : ℝ} (hP4 : QuantitativeCoarseGrainedEllipticity P) (hC_nonneg : 0 ≤ C) (m : ℕ) : have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sLower (hP4.sLower + β) m ≤ C * section52MomentLossCoeff d hP4.xi hP4.sLower (hP4.sLower + β) * Real.rpow 3 (-β * ↑m)