Coarse-graining support: Support.Book.Ch05.Theorems.Section56.SmallContrastJBound.Preliminaries

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

Section 5.6: small-contrast coarse-fluctuation iteration

This file formalizes the manuscript estimate e.J.upper.bound.coarse.fluctuations.small.contrast.final.

noncomputable def HCPolySupport.Book.Ch05.Section56.smallContrastFinalRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C : ℝ) (k m : ℕ) (e : Vec d) : ℝ

The four-term right side in e.J.upper.bound.coarse.fluctuations.small.contrast.final.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.smallContrastReducedRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C0 η : ℝ) (k m : ℕ) (e : Vec d) : ℝ

The reduced small-contrast response bound at scales k and m, combining coarse fluctuations, the special-vector tau term, scale decay, and squared contrast defect.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.vecNorm_eq_one_of_vecNormSq_eq_one {d : ℕ} {e : Vec d} (he : vecNormSq e = 1) : Ch02.vecNorm e = 1

theorem HCPolySupport.Book.Ch05.Section56.thetaAtScale_zero_le_widetildeThetaAtScale_zero_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) : thetaAtScale hP hStruct 0 ≤ widetildeThetaAtScale P 0 hP4

theorem HCPolySupport.Book.Ch05.Section56.thetaAtScale_le_two_of_widetildeThetaAtScale_zero_le_two {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) (m : ℕ) : thetaAtScale hP hStruct ↑m ≤ 2

theorem HCPolySupport.Book.Ch05.Section56.thetaAtScale_sub_one_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : 0 ≤ thetaAtScale hP hStruct ↑m - 1

theorem HCPolySupport.Book.Ch05.Section56.sqrt_sub_one_sq_le_theta_sub_one_sq {θ : ℝ} (hθ_one : 1 ≤ θ) : (√θ - 1) ^ 2 ≤ (θ - 1) ^ 2

theorem HCPolySupport.Book.Ch05.Section56.quarter_theta_sub_one_le_sqrt_sub_one {θ : ℝ} (hθ_one : 1 ≤ θ) (hθ_two : θ ≤ 2) : 1 / 4 * (θ - 1) ≤ √θ - 1

theorem HCPolySupport.Book.Ch05.Section56.expectedResponseJCubeSet_special_ge_quarter_theta_sub_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) (m : ℕ) (e : Vec d) (he : vecNormSq e = 1) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; 1 / 4 * (thetaAtScale hP hStruct ↑m - 1) ≤ Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e

theorem HCPolySupport.Book.Ch05.Section56.expectedResponseJCubeSet_special_le_two_expectedCenteredResponseJAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : vecNormSq e = 1) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ 2 * expectedCenteredResponseJAtScale hP hStruct (↑m) p_e q_e

theorem HCPolySupport.Book.Ch05.Section56.coarseFluctuationScalarWeightAtScale_le_four_of_smallContrast {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) (m : ℕ) : Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m ≤ 4

theorem HCPolySupport.Book.Ch05.Section56.coarseFluctuationResponseMomentAtScale_le_zero {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (_hkm : k ≤ m) (e : Vec d) : Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e ≤ Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 0 m e

theorem HCPolySupport.Book.Ch05.Section56.coarseFluctuationUnitMomentWeight_mul_responseMoment_le_sixteen_of_smallContrast {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) (he : vecNormSq e = 1) : Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e ≤ 16

theorem HCPolySupport.Book.Ch05.Section56.sum_range_to_Icc_descending {k m : ℤ} (hkm : k ≤ m) (F : ℕ → ℝ) : ∑ j ∈ Finset.range (m - k).toNat, F j = ∑ n ∈ Finset.Icc (k + 1) m, F (m - n).toNat

theorem HCPolySupport.Book.Ch05.Section56.sum_Icc_betaWeight_le_five_beta_inv {k m : ℤ} (hkm : k ≤ m) {β : ℝ} (hβ : 0 < β) (hβ_le : β ≤ 1) : ∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) ≤ 5 * β⁻¹

theorem HCPolySupport.Book.Ch05.Section56.expectedResponseJCubeSet_origin_eq_annealedResponseJAtScale {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (n : ℤ) (p q : Vec d) : Ch04.expectedResponseJCubeSet P (originCube d n) p q = Ch04.annealedResponseJAtScale P n p q

theorem HCPolySupport.Book.Ch05.Section56.expectedResponseJCubeSet_origin_eq_origin_add_tauAtScale {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (m k : ℤ) (p q : Vec d) : Ch04.expectedResponseJCubeSet P (originCube d k) p q = Ch04.expectedResponseJCubeSet P (originCube d m) p q + tauAtScale P m k p q

theorem HCPolySupport.Book.Ch05.Section56.tauAtScale_le_tauAtScale_of_left_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k n m : ℤ} (hk_nonneg : 0 ≤ k) (hkn : k ≤ n) (p q : Vec d) : tauAtScale P m n p q ≤ tauAtScale P m k p q

theorem HCPolySupport.Book.Ch05.Section56.coarseFluctuationTauSumAtScale_le_five_beta_inv_tauAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) : have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 k m e ≤ 5 * β⁻¹ * tauAtScale P (↑m) (↑k) p_e q_e

theorem HCPolySupport.Book.Ch05.Section56.exists_decay_absorption_const {β A : ℝ} (hβ : 0 < β) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {n : ℕ}, C ≤ ↑n → A * Real.rpow 3 (-2 * β * ↑n) ≤ 1 / 4

theorem HCPolySupport.Book.Ch05.Section56.section53CoarseFluctuationBetaCoreParams_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBetaCoreParams params

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

theorem HCPolySupport.Book.Ch05.Section56.self_le_half_add_of_le {x R : ℝ} (h : x ≤ 1 / 2 * x + R) : x ≤ 2 * R

theorem HCPolySupport.Book.Ch05.Section56.coarseFluctuationYoungManuscriptRHSAtScale_eq_decomp {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C ε η : ℝ) (k m : ℕ) (e : Vec d) : Section53.JUpperBoundCoarseFluctuations.coarseFluctuationYoungManuscriptRHSAtScale hP hStruct hP4 C ε η k m e = have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; have θ := thetaAtScale hP hStruct ↑m; have scalarWeight := Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m; have fluctuationSum := Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m; have tauSum := Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 k m e; have unitMomentWeight := Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m; have responseMoment := Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e; C * (η * Ch04.expectedResponseJCubeSet P (originCube d ↑k) p_e q_e + η⁻¹ * tauAtScale P (↑m) (↑k) p_e q_e) + C * ε * (√θ - 1) ^ 2 + C * ε⁻¹ * β⁻¹ * θ * fluctuationSum + C * ε⁻¹ * (β ^ 2)⁻¹ * scalarWeight * tauSum + C * ↑hP4.xi * ε⁻¹ * (β ^ 3)⁻¹ * Real.rpow 3 (-β * ↑m) * unitMomentWeight * responseMoment + C * ε⁻¹ * (β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k)) * scalarWeight * (θ - 1)

theorem HCPolySupport.Book.Ch05.Section56.two_mul_sum_six_le {a₁ a₂ a₃ a₄ a₅ a₆ b₁ b₂ b₃ b₄ b₅ b₆ : ℝ} (h₁ : 2 * a₁ ≤ b₁) (h₂ : 2 * a₂ ≤ b₂) (h₃ : 2 * a₃ ≤ b₃) (h₄ : 2 * a₄ ≤ b₄) (h₅ : 2 * a₅ ≤ b₅) (h₆ : 2 * a₆ ≤ b₆) : 2 * (a₁ + a₂ + a₃ + a₄ + a₅ + a₆) ≤ b₁ + b₂ + b₃ + b₄ + b₅ + b₆

theorem HCPolySupport.Book.Ch05.Section56.young_rhs_two_mul_le_sum_of_term_bounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C η : ℝ) (k m : ℕ) (e : Vec d) (B₁ B₂ B₃ B₄ B₅ B₆ : ℝ) (h₁ : 2 * (C * (η * Ch04.expectedResponseJCubeSet P (originCube d ↑k) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e) + η⁻¹ * tauAtScale P (↑m) (↑k) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e))) ≤ B₁) (h₂ : 2 * (C * (√(thetaAtScale hP hStruct ↑m) - 1) ^ 2) ≤ B₂) (h₃ : 2 * (C * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4)⁻¹ * thetaAtScale hP hStruct ↑m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m) ≤ B₃) (h₄ : 2 * (C * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 2)⁻¹ * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 k m e) ≤ B₄) (h₅ : 2 * (C * ↑hP4.xi * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 3)⁻¹ * Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m) * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e) ≤ B₅) (h₆ : 2 * (C * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 2)⁻¹ * Real.rpow 3 (-2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑(m - k)) * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationScalarWeightAtScale hP hStruct m * (thetaAtScale hP hStruct ↑m - 1)) ≤ B₆) : 2 * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationYoungManuscriptRHSAtScale hP hStruct hP4 C 1 η k m e ≤ B₁ + B₂ + B₃ + B₄ + B₅ + B₆

theorem HCPolySupport.Book.Ch05.Section56.small_contrast_rest_sum_eq (J tauCoeff₁ tauCoeff₂ tau thetaTerm fluctTerm tailTerm : ℝ) : 1 / 4 * J + tauCoeff₁ * tau + thetaTerm + fluctTerm + tauCoeff₂ * tau + tailTerm + 1 / 4 * J = 1 / 2 * J + (fluctTerm + (tauCoeff₁ + tauCoeff₂) * tau + tailTerm + thetaTerm)

theorem HCPolySupport.Book.Ch05.Section56.small_contrast_rest_sum_terms_eq (J tauTerm₁ tauTerm₂ thetaTerm fluctTerm tailTerm : ℝ) : 1 / 4 * J + tauTerm₁ + thetaTerm + fluctTerm + tauTerm₂ + tailTerm + 1 / 4 * J = 1 / 2 * J + (fluctTerm + (tauTerm₁ + tauTerm₂) + tailTerm + thetaTerm)

theorem HCPolySupport.Book.Ch05.Section56.absorb_quarter_terms {J tauTerm₁ tauTerm₂ thetaTerm fluctTerm tailTerm : ℝ} (h : J ≤ 1 / 4 * J + tauTerm₁ + thetaTerm + fluctTerm + tauTerm₂ + tailTerm + 1 / 4 * J) : J ≤ 2 * (fluctTerm + (tauTerm₁ + tauTerm₂) + tailTerm + thetaTerm)