Documentation

LeanPool.HighContrastHomogenization.Entry.Multiscale.OneGrid.Recurrence

High-contrast homogenization: Entry.Multiscale.OneGrid.Recurrence #

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

Step 2 β€” the powered parent–child recurrence #

Group E of the printed proof (p.fixed.geometry.one.grid.propagation), first part: the parent–child recurrence as this decomposition consumes it, the bridge between the mixed Schatten norm and the profile's printed moment, and the powered form e.fixed.geometry.parent.child.powered.

Part of the proof of HCPoly/Entry/Statements/OneGridPropagation.lean. Conventions of the group: q = 𝒬(π”ͺ) is Geometry.explicitRoundedGrid jStar metric at every loss, history, profile and drift; metric (not m) names the positive matrix, because m, n, mβ‚€ are generations; the source lower scale e.source.lower.scale is carried exactly by the source-facing declaration HCPoly/Entry/OneGridPropagation.lean; this group's stronger internal algebraic and history lemmas omit an unused threshold, and this group's generic integration helpers take finiteness, integrability or measurability inputs that are proved at their actual use sites, not extra premises of the printed proposition.

Group E. Step 2 β€” profile contraction (p.fixed.geometry.one.grid.propagation) #

source
theorem HCPolySupport.HighContrast.Multiscale.parent_child_recurrence_input (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) :
βˆƒ (Csrc : ℝ), 0 < Csrc ∧ βˆ€ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ξ¨ : ℝ β†’ ℝ) (K : ℝ) (S : CoeffSpace d β†’ ℝ), MeasureTheory.IsProbabilityMeasure P β†’ IsStationaryLaw P β†’ IsUnitRangeLaw P β†’ CoarseEllipticityDagger P Ξ³ E Ξ¨ K S β†’ βˆ€ (N : β„•), 2 ≀ N β†’ Even N β†’ βˆ€ (jStar : β„•), 2 * d ≀ 3 ^ jStar β†’ ⌈Csrc * Real.logb 3 (2 * K)βŒ‰ ≀ ↑jStar β†’ βˆ€ (m : Mat d), Matrix.PosDef m β†’ βˆ€ (j h : β„€), ↑jStar ≀ j β†’ 1 ≀ h β†’ lqSchattenNorm P (↑N) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) (j + h)) ≀ ↑N * 3 ^ (↑d / 2) * (1 + (2 * ↑d) ^ (↑N)⁻¹) * 3 ^ (-(↑d / 2) * ↑h) * Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) * lqSchattenNorm P (↑N) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) j) + 2 * (1 + ↑d ^ (1 - (↑N)⁻¹)) * Real.exp ((1 - (↑N)⁻¹) * detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) * (Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) - 1) ^ (↑N)⁻¹

The parent–child recurrence, p.fixed.geometry.parent.child.recurrence (p.fixed.geometry.parent.child.recurrence), repeated here with the exact type of HCPolySupport.HighContrast.Entry.fixed_geometry_parent_child_recurrence.

This bridge is discharged by one exact application of the Entry.fixed_geometry_parent_child_recurrence; its elaborated type is identical to that of the theorem it applies.

source
theorem HCPolySupport.HighContrast.Multiscale.lqSchattenNorm_pow_eq_integral (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ξ¨ : ℝ β†’ ℝ) (K : ℝ) (S : CoeffSpace d β†’ ℝ) :
MeasureTheory.IsProbabilityMeasure P β†’ IsStationaryLaw P β†’ IsUnitRangeLaw P β†’ CoarseEllipticityDagger P Ξ³ E Ξ¨ K S β†’ βˆ€ (jStar : β„•), 2 * d ≀ 3 ^ jStar β†’ βˆ€ (metric : Mat d), Matrix.PosDef metric β†’ βˆ€ (j : β„€), lqSchattenNorm P (↑(bigQ d Ξ³)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j) ^ bigQ d Ξ³ = ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d Ξ³)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d Ξ³ βˆ‚P

The bridge between the recurrence's mixed norm β€–Β·β€–_{L^Q(S_Q)} and the profile's printed moment E[|V^q_j|_{S_Q}^Q]: the Q-th power of the first is the second. The real Schatten index and the natural outer power are exactly as HCPoly/Entry/Setup/Profile.lean records.

source
theorem HCPolySupport.HighContrast.Multiscale.parent_child_powered (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) :
βˆƒ (Csrc : ℝ), 0 < Csrc ∧ βˆ€ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ξ¨ : ℝ β†’ ℝ) (K : ℝ) (S : CoeffSpace d β†’ ℝ), MeasureTheory.IsProbabilityMeasure P β†’ IsStationaryLaw P β†’ IsUnitRangeLaw P β†’ CoarseEllipticityDagger P Ξ³ E Ξ¨ K S β†’ βˆ€ (jStar : β„•), 2 * d ≀ 3 ^ jStar β†’ ⌈Csrc * Real.logb 3 (2 * K)βŒ‰ ≀ ↑jStar β†’ βˆ€ (metric : Mat d), Matrix.PosDef metric β†’ βˆ€ (j h : β„€), ↑jStar ≀ j β†’ 1 ≀ h β†’ ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d Ξ³)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) (j + h) a) ^ bigQ d Ξ³ βˆ‚P ≀ 2 ^ (bigQ d Ξ³ - 1) * (3 ^ d * ↑(bigQ d Ξ³)) ^ bigQ d Ξ³ * 3 ^ (-(↑(bigQ d Ξ³) * ↑d / 2) * ↑h) * Real.exp (↑(bigQ d Ξ³) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j (j + h)) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d Ξ³)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d Ξ³ βˆ‚P + 2 ^ (2 * bigQ d Ξ³ - 1) * (1 + ↑d ^ (1 - (↑(bigQ d Ξ³))⁻¹)) ^ bigQ d Ξ³ * (Real.exp (↑(bigQ d Ξ³) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j (j + h)) - 1)

e.fixed.geometry.parent.child.powered (p.fixed.geometry.one.grid.propagation): apply the recurrence with N = Q, raise to the Q-th power using (a+b)^Q ≀ 2^{Q-1}(a^Q + b^Q) and e^{(Q-1)t}(e^t-1) ≀ e^{Qt}-1.