Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.YoungRHS

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

YoungRHS

The standard coarse-fluctuation estimate contains the initial term sqrt(tau_{m,k}) * sqrt(E[J_k]). For the flatness-rules route we need the same theorem with this term treated by Young, yielding eta * E[J_k] + eta^{-1} * tau_{m,k}. This file derives that theorem from the already proved Section 5.3 coarse-fluctuation estimate by a scalar comparison of right-hand sides.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationYoungManuscriptRHSAtScale {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 coarse-fluctuation manuscript RHS with the initial square-root term replaced by its Young envelope.

Equations

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

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationManuscriptRHSAtScale_le_youngManuscriptRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {C ε η : ℝ} (hC : 0 ≤ C) (hη : 0 < η) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) : coarseFluctuationManuscriptRHSAtScale hP hStruct hP4 C ε k m e ≤ coarseFluctuationYoungManuscriptRHSAtScale hP hStruct hP4 C ε η k m e

Scalar comparison of the standard Section 5.3 coarse-fluctuation RHS with the Young-envelope RHS.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.JUpperBoundCoarseFluctuations_young_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {k m : ℕ}, k < m → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ε η : ℝ}, 0 < ε → ε ≤ 1 → 0 < η → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; expectedCenteredResponseJAtScale hP hStruct (↑m) p_e q_e ≤ coarseFluctuationYoungManuscriptRHSAtScale hP hStruct hP4 C ε η k m e

Section 5.3 coarse-fluctuation bound with the initial square-root term replaced by the Young envelope.