Documentation

LeanPool.HighContrastHomogenization.Entry.Multiscale.OneGrid.HistoryMajorization

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

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

Step 1 β€” the histories are majorized by the profile #

Group D of the printed proof (p.fixed.geometry.one.grid.propagation), second half: the fluctuation decomposition, the mean-history estimates, and conjuncts 1 and 5, e.fixed.geometry.profile.majorization and e.fixed.geometry.carried.majorization.

Part of the proof of the statement in HCPoly/Entry/Statements/OneGridPropagation.lean. Group conventions: 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 statement in HCPoly/Entry/OneGridPropagation.lean; this group's stronger 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.

source
theorem HCPolySupport.HighContrast.Multiscale.fluctuationHistory_decompose (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ fluctuationHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m ≀ 3 ^ (-((1 - Ξ³) / 4) * (↑m - ↑n)) * (1 + meanPenalty (bigQ d Ξ³) (relMean P (Geometry.explicitRoundedGrid jStar metric) n m)) * fluctuationHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar n + βˆ‘ j ∈ Finset.Icc (n + 1) m, 3 ^ (-((1 - Ξ³) / 4) * (↑m - ↑j)) * Real.exp (↑(bigQ d Ξ³) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j m) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d Ξ³)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d Ξ³ βˆ‚P

The printed fluctuation estimate of Step 1 (p.fixed.geometry.one.grid.propagation): change of normalization for the generations up to n, and a cell-wise bound for the remaining generations, using Qρ_max - d β‰₯ ΒΌ(1-Ξ³). The right-hand side is the fluctuation part of 𝒫_q(m;n).

source
theorem HCPolySupport.HighContrast.Multiscale.fluctuationHistory_le_profile (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ fluctuationHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m ≀ profile P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar n m

β„‹^fluc_q(m) ≀ 𝒫_q(m;n) with coefficient one (p.fixed.geometry.one.grid.propagation).

source
theorem HCPolySupport.HighContrast.Multiscale.meanHistory_lower_part_le (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ βˆ‘ j ∈ Finset.Ico (↑jStar) n, 3 ^ (-((1 - Ξ³) / 4) * (↑m - 1 - ↑j)) * meanPenalty (bigQ d Ξ³) (relMean P (Geometry.explicitRoundedGrid jStar metric) j m) ≀ 3 ^ (-((1 - Ξ³) / 4) * (↑m - ↑n)) * (1 + meanPenalty (bigQ d Ξ³) (relMean P (Geometry.explicitRoundedGrid jStar metric) n m)) * meanHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) (↑jStar) n + 3 ^ (-((1 - Ξ³) / 4) * (↑m - ↑n)) * meanPenalty (bigQ d Ξ³) (relMean P (Geometry.explicitRoundedGrid jStar metric) n m) * βˆ‘ j ∈ Finset.Ico (↑jStar) n, 3 ^ (-((1 - Ξ³) / 4) * (↑n - 1 - ↑j))

The printed estimate for the mean-history terms below n (p.fixed.geometry.one.grid.propagation): multiply the composed penalty by 3^{-ΒΌ(1-Ξ³)(m-1-j)} and sum over j_* ≀ j < n.

source
theorem HCPolySupport.HighContrast.Multiscale.meanHistory_le_profile (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) :
βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ meanHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) (↑jStar) m ≀ C * profile P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar n m

β„‹^mean_q(m) ≀ C 𝒫_q(m;n) (p.fixed.geometry.one.grid.propagation): the geometric sum is bounded by C, the first term by the first term of the profile, and β€” when m > n β€” the leftover penalty by the j = n term of β„‹^mean_q(m;n); when m = n that leftover vanishes.

source
theorem HCPolySupport.HighContrast.Multiscale.history_le_profile (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) :
βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ history P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m ≀ C * profile P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar n m

Conjunct 1, e.fixed.geometry.profile.majorization: the profile majorizes the history.

source
theorem HCPolySupport.HighContrast.Multiscale.carried_history_majorization (d : β„•) (hd : 2 ≀ d) (Ξ³ : ℝ) (hΞ³ : Ξ³ ∈ Set.Ico 0 1) :
βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (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 β†’ βˆ€ (n m : β„€), ↑jStar ≀ n β†’ n ≀ m β†’ fluctuationHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m + meanHistory P Ξ³ (Geometry.explicitRoundedGrid jStar metric) (↑jStar) m + determinantDrift P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m ≀ C * (profile P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P Ξ³ (Geometry.explicitRoundedGrid jStar metric) jStar m)

Conjunct 5, e.fixed.geometry.carried.majorization (p.fixed.geometry.one.grid.propagation): the same majorization with the determinant drift carried on both sides.