High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.RootTheorem

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The root at the frozen signature, with no hypothesis

HCPoly.Provider.PolynomialHomogenization.Root.CorrectorComposition.RootOfBallTriangle inhabits the frozen statement on one named analytic hypothesis, ExactRootBallTriangle, and HCPoly.Provider.PolynomialHomogenization.Root.CorrectorComposition.BallTriangle proves that hypothesis. This module composes the two, so the frozen statement is inhabited at the frozen signature (d : ℕ) (hd : 2 ≤ d) with no hypothesis and no NeZero d binder — the instance is derived from hd inside, exactly as the frozen declaration's own signature requires.

The type below is the frozen statement's type, taken from HCPoly.Provider.PolynomialHomogenization.Root.CorrectorComposition.RootOfBallTriangle; nothing here restates it.

theorem HCPolySupport.HighContrast.CorrectorComposition.polynomial_homogenization_root (d : ℕ) (hd : 2 ≤ d) : ∃ (cd : ℝ) (C₀ : ℝ → ℝ → ℝ → ℝ), 0 < cd ∧ (∀ (s₀ ρ Rad : ℝ), 0 < C₀ s₀ ρ Rad) ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (cSrc : ℝ) (κ : ℝ) (C₁ : ℝ → ℝ), 0 < C ∧ 0 < cSrc ∧ 0 < κ ∧ (∀ (ϑ : ℝ), 0 < C₁ ϑ) ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∃ (abar : Mat d) (Lpoly : ℝ) (X : CoeffSpace d → ℝ) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), 1 ≤ Lpoly ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • gradPhi e a x + gradPhi e' a x) ∧ (∀ (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d), gradPhi e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => gradPhi e a (x + Source.AKL.intTranslation z)) ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ (∀ (t : ℝ), 1 ≤ t → P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ (↑d - 2 * g)) + (Ψ (cSrc * t))⁻¹) ∧ (∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul (symmPart abar) x)) ∧ ∃ (Ωend : Set (CoeffSpace d)), MeasurableSet Ωend ∧ P.real Ωend = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' Ωend = Ωend) ∧ (∀ s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2), ∀ (ρ Rad : ℝ) (U : Set (Vec d)), (∃ (j : ℤ) (z : Vec d), U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) → HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) ρ Rad → U ⊆ ellipsoid abar 1 → ellipsoid abar (1 / (3 * √↑d)) ⊆ U → ∀ a ∈ Ωend, ⋯) ∧ (∀ a ∈ Ωend, ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a) ∧ IsWeakSolutionOn (fun (x : Vec d) => ↑↑a x) Set.univ fun (x : Vec d) => e + gradPhi e a x) ∧ (∀ a ∈ Ωend, ∀ (e : Vec d) (r : ℝ), X a ≤ r → (ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (x : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a x)) + ENNReal.ofReal r⁻¹ * ⋯ ≤ ENNReal.ofReal (C * √(vecDot e (matVecMul (symmPart abar) e)) * (r / X a) ^ (-κ))) ∧ (∀ a ∈ Ωend, ∀ ϑ ∈ Set.Ioo 0 1, (∀ (v : Vec d → ℝ) (Dv : Vec d → Vec d), ⋯) ∧ ∀ (e : Vec d) (c : ℝ), ⋯) ∧ ∀ a ∈ Ωend, ∀ (R : ℝ), X a ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), ⋯ → ⋯

The frozen root statement, inhabited unconditionally.