High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.LargeScaleC1AtCertificate

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

the large-scale C¹ slope approximation clause at an arbitrary certificate

The C¹ slope approximation at the exact-gauge terminal fixes reconciledRootGoodScale d cStar in both its certificate slot and its terminal premise. The terminal is proved at the event-retaining certificate reconciledRootGoodScaleOn, because the pushforward marker's own carrier is only available on the invariant core the event supplies. This module is the same theorem with the certificate a parameter; the proof body is the one, with g and κc already fixed.

theorem HCPolySupport.HighContrast.CorrectorComposition.largeScaleC1_of_terminal_atCertificate (d : ℕ) [NeZero d] (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) (CorrectorFamily : Mat d → (Vec d → CoeffSpace d → Vec d → ℝ) → (Vec d → CoeffSpace d → Vec d → Vec d) → Prop) (hposDef : ∀ (abar : Mat d) (a : CoeffSpace d) (x : ℝ), GoodScale abar a x → Matrix.PosDef (symmPart abar)) (hlinear : ∀ (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi → ∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (y : Vec d) => c • gradPhi e a y + gradPhi e' a y) (hterminal : ∀ eta ∈ Set.Ioo 0 1, ExactRootGaugeTerminal d GoodScale CorrectorFamily eta) : ∃ (C₁ : ℝ → ℝ), (∀ (ϑ : ℝ), 0 < C₁ ϑ) ∧ ∀ (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), CorrectorFamily abar Phi gradPhi → ∀ (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale abar a x → ∀ (R : ℝ), x ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du → ∀ ϑ ∈ Set.Ioo 0 1, ∃ (e : Vec d), ∀ r ∈ Set.Icc x R, (weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) => Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (C₁ ϑ * (r / R) ^ ϑ) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du

the large-scale C¹ slope approximation clause at a given certificate, from the exact-gauge terminal.