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

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

Assembly of the one-step contraction

This file combines the Section 5.3 centered-response estimate, the good-scale RHS compression, and the centered-response identity to prove the public Section 5.4 one-step contraction proposition.

def HCPolySupport.Book.Ch05.Section54.OneStepContraction.unitCoordinateVector {d : ℕ} [NeZero d] : Vec d

The first coordinate unit vector, used as a fixed unit direction in the one-step contraction estimates.

Equations

• HCPolySupport.Book.Ch05.Section54.OneStepContraction.unitCoordinateVector = Pi.single 0 1

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparationConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only one-step scale-separation constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarsePairLinearBudgetConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only linear budget constant for Section 5.3-beta full-block sums.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepWeightedRefinedBudgetConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only refined budget constant for Section 5.3-beta full-block sums.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only full-block constant for the one-step RHS compression.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only tau-sum constant for the one-step RHS compression.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCompressionMultiplierParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only multiplier compressing the Section 5.3 manuscript RHS. The outer max gives a nonnegative witness without exposing any proof package.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparationConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : oneStepScaleSeparationConstParams hP4.params = oneStepScaleSeparationConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarsePairLinearBudgetConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : oneStepCoarsePairLinearBudgetConstParams hP4.params = oneStepCoarsePairLinearBudgetConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepWeightedRefinedBudgetConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : oneStepWeightedRefinedBudgetConstParams hP4.params = oneStepWeightedRefinedBudgetConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : oneStepCoarseFullBlockConstParams hP4.params = oneStepCoarseFullBlockConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseTauSumConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : oneStepCoarseTauSumConstParams hP4.params = oneStepCoarseTauSumConst hP4

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.exists_expectedCenteredResponseJAtScale_special_le_compressed {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {Csep delta epsilon : ℝ} {m : ℕ}, oneStepScaleSeparationConstParams params ≤ Csep → 0 < delta → delta ≤ 1 / 2 → Csep * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m → 0 < epsilon → epsilon ≤ 1 → hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m → (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ → ∀ (e : Vec d), Ch02.vecNorm e = 1 → expectedCenteredResponseJAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e) ≤ K * ((epsilon + epsilon⁻¹ * √delta) * thetaAtScale hP hStruct 0)

Compressed form of the Section 5.3 input at a good scale.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContraction_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 → ∀ {m : ℕ}, C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m → hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m → (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ → thetaAtScale hP hStruct ↑m ≤ 1 + C * delta.rpow (1 / 4) * thetaAtScale hP hStruct 0

Proposition p.one.step.contraction.homogenization.scale from the manuscript.