High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.IntrinsicCorrectorEvent

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

The intrinsic convergence event of the physical corrector family

A coefficient sample carries a corrector family as soon as some triadic coefficient family represents it on every centered cube, its finite affine corrections converge locally, and the weak-error row is summable below the threshold at which reverse Liouville classification identifies translated gradients. The datum recorded here is a property of the sample alone: it mentions no homogenized matrix, no contrast exponent, no rate, no probability law and no scale.

The event also mentions no order. The good-tail order at which the row is summable is a field of RootCorrectorData, hence existentially quantified by RootCorrectorEvent, so the event, the selected carrier rootJointCarrier, the pushforward core and the marker RootPushCorrectorFamilyPredicate are all independent of it. The order survives only where it belongs — in the supply, which may choose it after the contrast exponent g.

The fixed private exponents

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorGrowth : ℝ

The sublinear growth exponent used by the Liouville classification.

Equations

• HCPolySupport.HighContrast.Root.rootCorrectorGrowth = 1 / 2

theorem HCPolySupport.HighContrast.Root.rootCorrectorGrowth_pos : 0 < rootCorrectorGrowth

theorem HCPolySupport.HighContrast.Root.rootCorrectorGrowth_lt_one : rootCorrectorGrowth < 1

The tolerances, at a free good-tail order

The three tolerances below are functions of the good-tail order s, admissible for every s in the corrector cone 0 < s < 1/2. Nothing else about the construction changes: the order is recorded as a field of the datum below, not as an index of the event, so the event, the selected carrier and the pushforward marker stay order-free.

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorIdentificationTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The tolerance below which the translated-gradient identification applies at the good-tail order s and the fixed growth exponent.

Equations

• HCPolySupport.HighContrast.Root.rootCorrectorIdentificationTolerance d s hs hs2 = Classical.choose ⋯

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorSlopeTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The tolerance below which a good tail already produces the local Cauchy property and the intrinsic normalization of every slope.

Equations

• HCPolySupport.HighContrast.Root.rootCorrectorSlopeTolerance d s hs hs2 = Classical.choose ⋯

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The tolerance used by the construction, at the order s.

Equations

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

theorem HCPolySupport.HighContrast.Root.rootCorrectorIdentification_spec (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : rootCorrectorIdentificationTolerance d s hs hs2 ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 (rootCorrectorIdentificationTolerance d s hs hs2) → ScalarIdentityGoodTail a s delta n → ∀ (PhiTarget : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation a PhiTarget → ∀ {b : CoeffField d}, IsAELocallyUniformlyElliptic b → (∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[MeasureTheory.volume.restrict (localGradientCube d q)] b) → ∀ (PhiSource : NormalizedLocalH1Carrier d) (e t : Vec d) (sRow N : ℝ) (q0 : ℕ), 0 < sRow → sRow < 1 / 2 → HasIntrinsicNormalizedSlope e PhiSource → (∀ (e' : Vec d), HasIntrinsicNormalizedSlope e' (PhiTarget e')) → (∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) sRow fun (x : Vec d) => e + PhiSource.globalGradientRepresentative x) ≤ N) → ∀ {v : Vec d → ℝ}, (MemLiouvilleClass b rootCorrectorGrowth v fun (x : Vec d) => e + PhiSource.globalGradientRepresentative (x + t)) → (fun (x : Vec d) => PhiSource.globalGradientRepresentative (x + t)) =ᵐ[MeasureTheory.volume] (PhiTarget e).globalGradientRepresentative

theorem HCPolySupport.HighContrast.Root.rootCorrectorSlope_spec (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : rootCorrectorSlopeTolerance d s hs hs2 ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 (rootCorrectorSlopeTolerance d s hs hs2) → ScalarIdentityGoodTail a s delta n → ∀ (e : Vec d), ∃ (hloc : FiniteAffineCorrectionLocalCauchy a), HasIntrinsicNormalizedSlope e (finiteAffineCorrectionJointLocalLimit a hloc e)

theorem HCPolySupport.HighContrast.Root.rootCorrectorTolerance_pos (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : 0 < rootCorrectorTolerance d s hs hs2

theorem HCPolySupport.HighContrast.Root.mem_identificationTolerance_of_mem {d : ℕ} [NeZero d] {s : ℝ} {hs : 0 < s} {hs2 : s < 1 / 2} {delta : ℝ} (h : delta ∈ Set.Ioc 0 (rootCorrectorTolerance d s hs hs2)) : delta ∈ Set.Ioc 0 (rootCorrectorIdentificationTolerance d s hs hs2)

theorem HCPolySupport.HighContrast.Root.mem_slopeTolerance_of_mem {d : ℕ} [NeZero d] {s : ℝ} {hs : 0 < s} {hs2 : s < 1 / 2} {delta : ℝ} (h : delta ∈ Set.Ioc 0 (rootCorrectorTolerance d s hs hs2)) : delta ∈ Set.Ioc 0 (rootCorrectorSlopeTolerance d s hs hs2)

theorem HCPolySupport.HighContrast.Root.exists_cauchy_intrinsic_of_goodTail {d : ℕ} [NeZero d] {s : ℝ} (hs : 0 < s) (hs2 : s < 1 / 2) (aFin : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ) (hmem : delta ∈ Set.Ioc 0 (rootCorrectorTolerance d s hs hs2)) (hgood : ScalarIdentityGoodTail aFin s delta n) : ∃ (hCauchy : FiniteAffineCorrectionLocalCauchy aFin), ∀ (e : Vec d), HasIntrinsicNormalizedSlope e (finiteAffineCorrectionJointLocalLimit aFin hCauchy e)

A summable weak-error row below the tolerance already yields local convergence of the finite affine corrections together with the intrinsic normalization of every slope.

The zero carrier

noncomputable def HCPolySupport.HighContrast.Root.zeroNormalizedCarrier (d : ℕ) : NormalizedLocalH1Carrier d

The zero normalized local carrier, used off the convergence event.

Equations

• HCPolySupport.HighContrast.Root.zeroNormalizedCarrier d = { value := 0, gradient := 0, graph := ⋯, unitMeanZero := ⋯ }

The intrinsic datum

structure HCPolySupport.HighContrast.Root.RootCorrectorData (d : ℕ) [NeZero d] (a : CoeffSpace d) : Type

Everything the construction reads off one coefficient sample: a triadic family representing it, local convergence of the finite affine corrections, a summable weak-error row below the identification tolerance, the intrinsic normalization of every slope, and the two rows of the limit: the scale-linear value growth and the weak gradient row.

• order : ℝ

  The good-tail order. The order at which the weak-error row of this datum is read is a field, not an index: it is existentially quantified by RootCorrectorEvent below, so neither the event, nor the selected carrier, nor the pushforward marker mentions it. Any order in the corrector cone 0 < s < 1/2 is admitted, and CorrectorComposition.jointLocalLimit_eq_of_aeeq shows that data of different orders for the same sample carry literally the same joint local limit — which is what makes the carrier well defined without an index.

• order_pos : 0 < self.order
• order_lt : self.order < 1 / 2
• aFin : Book.Ch02.TriadicCoeffFamily d

  A triadic coefficient family for the sample.

• hCauchy : FiniteAffineCorrectionLocalCauchy self.aFin

  Its finite affine corrections converge locally at every slope.

• tolerance : ℝ

  The weak-error tolerance.

• start : ℤ

  The generation at which the weak-error row is read.

• tolerance_mem : self.tolerance ∈ Set.Ioc 0 (rootCorrectorTolerance d self.order ⋯ ⋯)
• goodTail : ScalarIdentityGoodTail self.aFin self.order self.tolerance self.start
• coeff (q : ℕ) : Book.Ch03.publicCoeffField (originCube d ↑q) self.aFin =ᵐ[MeasureTheory.volume.restrict (localGradientCube d q)] fun (x : Vec d) => ↑↑a x
• coeffAll (Q : TriadicCube d) : (self.aFin.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a x

  The all-cube representation. The reference family represents the sample on every triadic cube, not only on the origin cubes, and against coeffOn rather than publicCoeffField. The converter that supplies the datum proves this pointwise (exists_shiftedNormalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow's hcoeffRef); keeping it in the a.e. form is enough for every consumer, and it is what makes the selected datum's family a.e. equal to the certificate's exact-gauge family as a Book.Ch02.TriadicCoeffFamily.AEEq.

• intrinsic (e : Vec d) : HasIntrinsicNormalizedSlope e (finiteAffineCorrectionJointLocalLimit self.aFin ⋯ e)
• valueGrowth (e : Vec d) : ∃ (q0 : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (q : ℕ), q0 ≤ q → cubeLpNorm (originCube d ↑q) 2 (finiteAffineCorrectionJointLocalLimit self.aFin ⋯ e).globalValueRepresentative ≤ C * 3 ^ q
• gradientGrowth (e : Vec d) : ∃ (q0 : ℕ) (N : ℝ), 0 ≤ N ∧ ∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) self.order fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit self.aFin ⋯ e).globalGradientRepresentative x) ≤ N

  The weak gradient row. The scale-uniform datum of the corrector gradient is its weak norm — the scale-normalized negative Besov norm of the affine-plus-corrector field — read at the datum's own order. It is the row the paper's corrector estimates publish, and it is law-free: no pointwise ellipticity pair enters it.

def HCPolySupport.HighContrast.Root.RootCorrectorEvent (d : ℕ) [NeZero d] (a : CoeffSpace d) : Prop

The intrinsic convergence event.

Equations

• HCPolySupport.HighContrast.Root.RootCorrectorEvent d a = Nonempty (HCPolySupport.HighContrast.Root.RootCorrectorData d a)

theorem HCPolySupport.HighContrast.Root.rootCorrectorEvent_of_goodTail {d : ℕ} [NeZero d] {a : CoeffSpace d} {s : ℝ} (hs : 0 < s) (hs2 : s < 1 / 2) (aFin : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ) (hmem : delta ∈ Set.Ioc 0 (rootCorrectorTolerance d s hs hs2)) (hgood : ScalarIdentityGoodTail aFin s delta n) (hcoeff : ∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) aFin =ᵐ[MeasureTheory.volume.restrict (localGradientCube d q)] fun (x : Vec d) => ↑↑a x) (hcoeffAll : ∀ (Q : TriadicCube d), (aFin.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a x) (hvalue : ∀ (hC : FiniteAffineCorrectionLocalCauchy aFin) (e : Vec d), ∃ (q0 : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (q : ℕ), q0 ≤ q → cubeLpNorm (originCube d ↑q) 2 (finiteAffineCorrectionJointLocalLimit aFin hC e).globalValueRepresentative ≤ C * 3 ^ q) (hgradient : ∀ (hC : FiniteAffineCorrectionLocalCauchy aFin) (e : Vec d), ∃ (q0 : ℕ) (N : ℝ), 0 ≤ N ∧ ∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit aFin hC e).globalGradientRepresentative x) ≤ N) : RootCorrectorEvent d a

The intrinsic datum is built from a summable weak-error row below the tolerance, the coefficient representation, and the two rows of the limit; local convergence and intrinsic normalization are discharged from the weak-error row itself.

The selected family

noncomputable def HCPolySupport.HighContrast.Root.selectedRootCorrectorData {d : ℕ} [NeZero d] (a : CoeffSpace d) (h : RootCorrectorEvent d a) : RootCorrectorData d a

The datum selected on the intrinsic event.

Equations

• HCPolySupport.HighContrast.Root.selectedRootCorrectorData a h = Classical.choice h

noncomputable def HCPolySupport.HighContrast.Root.rootJointCarrier (d : ℕ) [NeZero d] (e : Vec d) (a : CoeffSpace d) : NormalizedLocalH1Carrier d

The event-totalized normalized carrier family: the selected joint local limit on the event, the zero carrier off it. The selection precedes the slope.

Equations

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

theorem HCPolySupport.HighContrast.Root.rootJointCarrier_of_event {d : ℕ} [NeZero d] (e : Vec d) {a : CoeffSpace d} (h : RootCorrectorEvent d a) : rootJointCarrier d e a = finiteAffineCorrectionJointLocalLimit (selectedRootCorrectorData a h).aFin ⋯ e

Slope linearity of the selected family

theorem HCPolySupport.HighContrast.Root.rootJointCarrier_add {d : ℕ} [NeZero d] (e e' : Vec d) {a : CoeffSpace d} (h : RootCorrectorEvent d a) : rootJointCarrier d (e + e') a = (rootJointCarrier d e a).addCarrier (rootJointCarrier d e' a)

theorem HCPolySupport.HighContrast.Root.rootJointCarrier_smul {d : ℕ} [NeZero d] (c : ℝ) (e : Vec d) {a : CoeffSpace d} (h : RootCorrectorEvent d a) : rootJointCarrier d (c • e) a = NormalizedLocalH1Carrier.smulCarrier c (rootJointCarrier d e a)

The joint local equation of the selected family

theorem HCPolySupport.HighContrast.Root.finiteAffineCorrectionJointLocalLimit_isJointLocalEquation {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) : IsFiniteAffineCorrectionJointLocalEquation a (finiteAffineCorrectionJointLocalLimit a hCauchy)

Every selected joint local limit satisfies the named joint local equation.

theorem HCPolySupport.HighContrast.Root.rootJointCarrier_equation {d : ℕ} [NeZero d] {a : CoeffSpace d} (h : RootCorrectorEvent d a) (e : Vec d) : HasWeakGradientOn Set.univ (rootJointCarrier d e a).globalValueRepresentative (rootJointCarrier d e a).globalGradientRepresentative ∧ IsWeakSolutionOn (fun (x : Vec d) => ↑↑a x) Set.univ fun (x : Vec d) => e + (rootJointCarrier d e a).globalGradientRepresentative x

On the intrinsic event the selected family is a global weak solution of the corrector equation for the sample, and its canonical representatives are a weak-gradient pair.