High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.RootOfBallTriangle

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

The root at the frozen signature, on one analytic hypothesis

The large-scale C¹ slope approximation clause terminal exactRootGaugeTerminal_onReconciled_of_ballTriangle follows from one named analytic hypothesis, the weighted-energy triangle inequality on the exact-root pullback ball. The frozen statement is therefore inhabited here with that as its only hypothesis, at the frozen signature (d : ℕ) (hd : 2 ≤ d), the NeZero d instance being derived from hd inside rather than taken as a binder.

The remaining binders are supplied unchanged: the coupled providers, hhomogenized, the negative-Sobolev Dirichlet error clause bridge, the unconditional the stationary corrector family clause, the decay, Liouville and Lipschitz clauses, and the assembly.

Where the corrector constant is quantified

The statement selects C₁ : ℝ → ℝ after g and before the coefficient sample and the point. A corrector family whose delay and whose starting index are chosen after the sample cannot supply it: those two data would have to appear in C₁, which is already fixed by then.

The route taken avoids the delay rather than accommodating it. The certificate's own power tail is read at order printCertificateOrder g and at the starting index triadicCeilingIndex x, with no delay and no restart, so every constant the simultaneous-slope row needs depends on d, g and the tolerance alone, provided the corrector smallness stays below a threshold free of the coefficient law. polynomial_homogenization_root_of_ballTriangle below is stated at that binder order.

The root, at the frozen statement's own signature

theorem HCPolySupport.HighContrast.CorrectorComposition.polynomial_homogenization_root_of_ballTriangle (d : ℕ) (hd : 2 ≤ d) (htri : ExactRootBallTriangle 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 conditionally on the weighted-energy triangle inequality on the exact-root pullback ball alone. The type below is the frozen statement's type, unchanged, and the signature is the frozen one — (d : ℕ) (hd : 2 ≤ d) — with the NeZero d instance derived from hd rather than taken as a binder.