Coarse-graining support: Support.Book.Ch05.Theorems.Section57.HomogenizationErrorQuenched

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

Quenched finite-q homogenization-error corollary

This file converts the Section 5.7 minimal-scale theorem into a finite-q bound on \mathcal E_{r,\infty,q} above a single random scale.

theorem HCPolySupport.Book.Ch05.Section57.deterministic_unitEllipticity_bound_le_squareEnvelope {K θ D τ α : ℝ} {m : ℕ} (hKD : K * θ ^ 2 ≤ D ^ α) (hD : 0 < D) (hατ : α ≤ τ) : K * θ ^ 2 ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / D) ^ (-α))) ^ 2

theorem HCPolySupport.Book.Ch05.Section57.finset_univ_fin_two_sup'_if_eq_max {Ω : Type u_1} (X Y : Ω → ℝ) (ω : Ω) : (Finset.univ.sup' finset_univ_fin_two_sup'_if_eq_max._proof_1 fun (i : Fin 2) => if i = 0 then X ω else Y ω) = max (X ω) (Y ω)

theorem HCPolySupport.Book.Ch05.Section57.isBigO_gammaSigma_max_two_of_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {η AJ AU : ℝ} (hη : 0 < η) {XJ XU : Ω → ℝ} (hJ : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) XJ AJ) (hU : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) XU AU) : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) (fun (ω : Ω) => max (XJ ω) (XU ω)) ((3 * Real.log 2) ^ η⁻¹ * max AJ AU)

theorem HCPolySupport.Book.Ch05.Section57.exists_homogenizationErrorOnOriginCube_interpolated_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {σ τ r q : ℝ}, 0 < σ → max params.sUpper params.sLower < τ / 2 → α < τ / 2 → τ ≤ 1 → 0 ≤ r * q → 0 < (r - τ / 2) * q → 0 < q → have ηJ := finiteQuenchedTailExponent d σ τ; have ηU := finiteQuenchedTailExponent d σ (τ / 2); have η := min ηJ ηU; ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ (ha : Ch04.AELocallyUniformlyEllipticField aω) {m : ℕ}, X aω ≤ 3 ^ m → have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount (r - τ / 2) q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X aω) ^ (-α))

Finite-sigma minimal-scale control of the full finite-q homogenization error on origin cubes.

The random scale is the maximum of the J minimal scale and the localized unit-ellipticity minimal scale; all deterministic terms are collapsed into the single factor (3^m / X)^(-alpha/2).

theorem HCPolySupport.Book.Ch05.Section57.exists_homogenizationErrorOnOriginCube_uniformEndpoint_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {τ r q : ℝ}, max params.sUpper params.sLower < τ / 2 → α < τ / 2 → τ ≤ 1 → 0 ≤ r * q → 0 < (r - τ / 2) * q → 0 < q → have η := ↑d; ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct), hInf.params = params → ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hInf.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ (ha : Ch04.AELocallyUniformlyEllipticField aω) {m : ℕ}, X aω ≤ 3 ^ m → have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount (r - τ / 2) q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X aω) ^ (-α))

Endpoint (σ = ∞) minimal-scale control of the full finite-q homogenization error on origin cubes.

The random scale is the maximum of the endpoint J minimal scale and a deterministic unit-ellipticity scale depending on thetaHat; the latter is absorbed into the same exp(C log^2(2 + thetaHat)) prefactor.