High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentitySuccessorConstants

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

noncomputable def HCPolySupport.HighContrast.identitySuccessorLocalConstant (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) : ℝ

Chosen local comparison constant for the identity gauge at the supplied rounded geometry.

Equations

• HCPolySupport.HighContrast.identitySuccessorLocalConstant d g geom hg = Classical.choose ⋯

theorem HCPolySupport.HighContrast.identitySuccessorLocalConstant_spec (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) : 0 < identitySuccessorLocalConstant d g geom hg ∧ ∀ (aGauge : CoeffSpace d) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge)) → ∀ (m : ℤ) (e : Vec d), scalarIdentityWeakError aIdentity (printCertificateOrder g) (m - 1) ≤ 1 → scalarIdentityWeakError aIdentity (printCertificateOrder g) m ≤ 1 → scalarIdentityWeakError aIdentity (printCertificateOrder g) (m + 1) ≤ 1 → Book.Ch03.h1EnergyNormOnCube (originCube d (m - 1 - 2)) aIdentity (successorInnerRestriction aIdentity m e).toH1 ≤ identitySuccessorLocalConstant d g geom hg * (scalarIdentityWeakError aIdentity (printCertificateOrder g) m + scalarIdentityWeakError aIdentity (printCertificateOrder g) (m + 1)) * euclideanNorm e

noncomputable def HCPolySupport.HighContrast.identitySuccessorRecurrenceConstant (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ℝ

Chosen constant controlling the identity-gauge finite energy recurrence.

Equations

• HCPolySupport.HighContrast.identitySuccessorRecurrenceConstant d g geom hg hdual = Classical.choose ⋯

theorem HCPolySupport.HighContrast.identitySuccessorRecurrenceConstant_spec (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : 1 ≤ identitySuccessorRecurrenceConstant d g geom hg hdual ∧ ∀ (aGauge : CoeffSpace d) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge)) → ∀ (q m : ℤ) (e : Vec d), q ≤ m - 1 - 2 → ScalarIdentityGoodMaxOnInterval aIdentity (printCertificateOrder g) 1 q (m - 1 - 2) → ∀ h ∈ Finset.Icc q (m - 1 - 2), finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) h ≤ identitySuccessorRecurrenceConstant d g geom hg hdual * finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) (m - 1 - 2) + identitySuccessorRecurrenceConstant d g geom hg hdual * ∑ j ∈ Finset.Ioc h (m - 1 - 2), scalarIdentityWeakError aIdentity (printCertificateOrder g) j * finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) j

noncomputable def HCPolySupport.HighContrast.identitySuccessorEnergyConstant (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ℝ

Energy comparison constant given by twice the recurrence constant times the local constant.

Equations

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

noncomputable def HCPolySupport.HighContrast.identitySuccessorSmallness (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ℝ

Minimum of one half and the inverse of twice the recurrence constant.

Equations

• HCPolySupport.HighContrast.identitySuccessorSmallness d g geom hg hdual = min (1 / 2) (2 * HCPolySupport.HighContrast.identitySuccessorRecurrenceConstant d g geom hg hdual)⁻¹

theorem HCPolySupport.HighContrast.identitySuccessorEnergyConstant_pos (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : 0 < identitySuccessorEnergyConstant d g geom hg hdual

theorem HCPolySupport.HighContrast.identitySuccessorSmallness_mem (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : identitySuccessorSmallness d g geom hg hdual ∈ Set.Ioo 0 1