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

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

theorem HCPolySupport.Book.Ch05.Section55.section53CoarseFluctuationBetaParams_pos_shiftedOneStepContraction {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedParams_sUpper_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : params.sUpper + Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params < 1

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedParams_sLower_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : params.sLower + Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params < 1

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedParams_sum_lt_one {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : params.sUpper + Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params + (params.sLower + Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params) < 1

noncomputable def HCPolySupport.Book.Ch05.Section55.betaShiftedParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : QuantitativeCoarseGrainedEllipticityParams d

Parameter-only (P4) data with both regularity exponents shifted by the Section 5.3/5.5 exponent β.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section55.betaShiftedP4_params {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) : (betaShiftedP4 hP hStruct hP4).params = betaShiftedParams hP4.params

theorem HCPolySupport.Book.Ch05.Section55.shiftedOneStepContraction_homogenizationScale_of_local_shifted_budget {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {delta : ℝ}, 0 < delta → delta ≤ 1 / 2 → ∀ {k n : ℕ}, k ≤ n → C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * shiftedWidetildeThetaAtScale P (↑k) hP4 (Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params)) ≤ ↑(n - k) → hP.barSigmaAtScale hStruct ↑k ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑n → (hP.barSigmaStarAtScale hStruct ↑k)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑n)⁻¹ → thetaAtScale hP hStruct ↑n ≤ 1 + C * delta.rpow (1 / 4) * thetaAtScale hP hStruct ↑k

Shifted one-step contraction on a window [k,n], with the local shifted moment budget at scale k left explicit.

This is the direct dilation of Section 5.4 after shifting the (P4) exponents by one β. The constant is chosen from the parameter-only data before the law and the window.

theorem HCPolySupport.Book.Ch05.Section55.shiftedOneStepContraction_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {delta : ℝ}, 0 < delta → delta ≤ 1 / 2 → ∀ {k n : ℕ}, k ≤ n → C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑(n - k) → hP.barSigmaAtScale hStruct ↑k ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑n → (hP.barSigmaStarAtScale hStruct ↑k)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑n)⁻¹ → thetaAtScale hP hStruct ↑n ≤ 1 + C * delta.rpow (1 / 4) * thetaAtScale hP hStruct ↑k