High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.SlopeBoundedRow

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

The undelayed exact-gauge row, with its slope norm and its good tail exported

Root.exists_printOrderUndelayedExactGaugeRow returns a slope e and the simultaneous-slope estimate on the cubes Finset.Icc n m, and nothing else. Two further data are needed, and the proof already has them in hand:

• the slope norm euclideanNorm e ≤ Aslope * ‖Du‖_{Q_m}, exported by exists_scalarIdentityInfiniteCorrectorC1ConstantsWithSlope;
• the good tail ScalarIdentityGoodTail aIdentity (printCertificateOrder g) (c / 2) (triadicCeilingIndex x) together with the local-Cauchy witness, which is what lets a consumer feed the existing exists_scalarIdentityGoodTailJointWeightedGradientBoundConstant and obtain ‖e + ∇Φ_e‖_{Q_q} ≤ B * euclideanNorm e at every generation above the start.

Both are needed for the near-terminal band of the large-scale C¹ slope approximation's ball terminal, where the canonical outer cube of r overshoots every triadic cube contained in the ball of radius R, so the cube row is silent and the estimate must be closed by the corrector's own energy.

Nothing here is an estimate: the two statements below are the ones with extra conjuncts that their own proofs already produce.

theorem HCPolySupport.HighContrast.Root.exists_printOrderC1SmallnessCeilingWithSlope (d : ℕ) [NeZero d] (g eta : ℝ) (hg : g ∈ Set.Ico 0 1) (hetaHalf : 1 / 2 ≤ eta) (heta1 : eta < 1) : ∃ (A : ℝ) (Aslope : ℝ) (cMax : ℝ), 0 < A ∧ 0 < Aslope ∧ cMax ∈ Set.Ioo 0 1 ∧ cMax ≤ canonicalCorrectorSmallness d g hg ∧ ∀ (aIdentity : Book.Ch03.CoeffFamily d) (delta : ℝ) (n0 : ℤ), delta ∈ Set.Ioc 0 cMax → ScalarIdentityGoodTail aIdentity (printCertificateOrder g) delta n0 → FiniteAffineCorrectionLocalCauchy aIdentity ∧ ∀ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi → ∀ (n m : ℕ), n0 ≤ ↑n → n + 2 ≤ m → ∀ (u : Book.Ch03.CubeSolution (originCube d ↑m) aIdentity), ∃ (e : Vec d), euclideanNorm e ≤ Aslope * Book.Ch03.h1EnergyNormOnCube (originCube d ↑m) aIdentity u.toH1 ∧ ∀ q ∈ Finset.Icc n m, (weightedGradNorm (aIdentity.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (y : Vec d) => u.toH1.grad y - (e + (Phi e).globalGradientRepresentative y)) ≤ ENNReal.ofReal (A * Real.rpow 3 (-eta * ↑(m - q))) * weightedGradNorm (aIdentity.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) u.toH1.grad

The printed-order C¹ smallness ceiling, with the slope norm.

theorem HCPolySupport.HighContrast.Root.exists_printOrderUndelayedExactGaugeRowWithSlope (d : ℕ) [NeZero d] (g eta : ℝ) (hg : g ∈ Set.Ico 0 1) (hetaHalf : 1 / 2 ≤ eta) (heta1 : eta < 1) : ∃ (A : ℝ) (Aslope : ℝ) (cMax : ℝ), 0 < A ∧ 0 < Aslope ∧ cMax ∈ Set.Ioo 0 1 ∧ ∀ (c kappa : ℝ), 0 < c → c ≤ cMax → ∀ (abar : Mat d) (a : CoeffSpace d) (x : ℝ), PrintOrderQuantitativeNormalizedReferenceCertificate abar g (correctorTargetAmplitude c kappa) kappa x a → ∃ (hS : Matrix.PosDef (symmPart abar)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (_ : FiniteAffineCorrectionLocalCauchy aIdentity), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑((canonicalIdentityGeometry d g hg).centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) ∧ IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi ∧ ScalarIdentityGoodTail aIdentity (printCertificateOrder g) (c / 2) ↑(Quenched.triadicCeilingIndex x) ∧ ∀ (n m : ℕ), ↑(Quenched.triadicCeilingIndex x) ≤ ↑n → n + 2 ≤ m → ∀ (u : Book.Ch03.CubeSolution (originCube d ↑m) aIdentity), ∃ (e : Vec d), euclideanNorm e ≤ Aslope * Book.Ch03.h1EnergyNormOnCube (originCube d ↑m) aIdentity u.toH1 ∧ ∀ q ∈ Finset.Icc n m, (weightedGradNorm (aIdentity.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (y : Vec d) => u.toH1.grad y - (e + (Phi e).globalGradientRepresentative y)) ≤ ENNReal.ofReal (A * Real.rpow 3 (-eta * ↑(m - q))) * weightedGradNorm (aIdentity.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) u.toH1.grad

The undelayed exact-gauge simultaneous-slope row, with the slope norm, the local-Cauchy witness and the good tail exported.