Coarse-graining support: Support.Book.Ch05.Theorems.Section57.EllipticityFromMinimalScale #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Ellipticity control above the Section 5.7 minimal scale #
This file is the Phase 3 packaging step for the public homogenization theorem.
It combines the collapsed finite-q homogenization-error corollary with the
Chapter 2 lemma that controls multiscale ellipticity from \mathcal E.
theorem
HCPolySupport.Book.Ch05.Section57.weightedEllipticity_finite_two_le_of_homogenizationError_bound
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : Ch02.TriadicCoeffFamily d)
{s σ B : ℝ}
(hs : 0 < s)
(hσ : 0 < σ)
(hE :
Ch02.HomogenizationErrorOnCube Q s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 2) a
(scalarMatrix σ) ≤ B)
:
max (σ⁻¹ * Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)
(σ * (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹) ≤ 2 * ↑(Fintype.card (Fin d)) * (B ^ 2 + 1)
Deterministic Ch5-facing form of the Ch2 ellipticity-control lemma.
theorem
HCPolySupport.Book.Ch05.Section57.lambdaSq_inv_le_inv_sigma_mul_of_weightedEllipticity_le
{d : ℕ}
(Q : TriadicCube d)
(a : Ch02.TriadicCoeffFamily d)
{s σ M : ℝ}
(hσ : 0 < σ)
(hM :
max (σ⁻¹ * Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)
(σ * (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹) ≤ M)
:
theorem
HCPolySupport.Book.Ch05.Section57.sqrt_LambdaSq_mul_sqrt_lambdaSq_inv_le_of_weightedEllipticity_le
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : Ch02.TriadicCoeffFamily d)
{s σ M : ℝ}
(hs : 0 < s)
(hσ : 0 < σ)
(hM_nonneg : 0 ≤ M)
(hM :
max (σ⁻¹ * Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)
(σ * (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹) ≤ M)
:
√(Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a) * √(Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ M
theorem
HCPolySupport.Book.Ch05.Section57.exists_weightedEllipticityOnOriginCube_interpolated_expLogSq
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (α : ℝ),
0 < α ∧ ∀ {σ τ s : ℝ},
0 < σ →
max params.sUpper params.sLower < τ / 2 →
α < τ / 2 →
τ ≤ 1 →
0 ≤ s * 2 →
0 < (s - τ / 2) * 2 →
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 F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha;
have σ0 := barSigmaLimit hP hStruct;
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);
have G :=
(Ch02.geometricDiscount s 2 * (Ch02.geometricDiscount (s - τ / 2) 2)⁻¹).rpow
(1 / 2);
have R := √((3 ^ m / X aω) ^ (-α));
have M := 2 * ↑(Fintype.card (Fin d)) * ((G * A * R) ^ 2 + 1);
max
(σ0⁻¹ * Ch02.LambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F)
(σ0 * (Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2)
F)⁻¹) ≤ M ∧ (Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F)⁻¹ ≤ σ0⁻¹ * M ∧ √(Ch02.LambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F) * √(Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2)
F)⁻¹ ≤ M
Finite-sigma ellipticity control on origin cubes above the same random
minimal scale as the collapsed finite-q \mathcal E estimate.
theorem
HCPolySupport.Book.Ch05.Section57.exists_weightedEllipticityOnOriginCube_uniformEndpoint_expLogSq
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (α : ℝ),
0 < α ∧ ∀ {τ s : ℝ},
max params.sUpper params.sLower < τ / 2 →
α < τ / 2 →
τ ≤ 1 →
0 ≤ s * 2 →
0 < (s - τ / 2) * 2 →
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 F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha;
have σ0 := barSigmaLimit hP hStruct;
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);
have G :=
(Ch02.geometricDiscount s 2 * (Ch02.geometricDiscount (s - τ / 2) 2)⁻¹).rpow
(1 / 2);
have R := √((3 ^ m / X aω) ^ (-α));
have M := 2 * ↑(Fintype.card (Fin d)) * ((G * A * R) ^ 2 + 1);
max (σ0⁻¹ * Ch02.LambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F)
(σ0 * (Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2)
F)⁻¹) ≤ M ∧ (Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F)⁻¹ ≤ σ0⁻¹ * M ∧ √(Ch02.LambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2) F) * √(Ch02.lambdaSq (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 2)
F)⁻¹ ≤ M
Endpoint (σ = ∞) ellipticity control on origin cubes above the same
random minimal scale as the endpoint finite-q \mathcal E estimate.