High-contrast homogenization: Entry.Multiscale.OneGrid.HistoryCounting

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

Step 1 — counting, integrability and transport

Group D of the printed proof (p.fixed.geometry.one.grid.propagation), first half: the cell counts of an adapted grid, the integrability and domination facts for the history integrands, stationarity transport, and the pointwise bounds the fluctuation decomposition consumes.

Part of the proof of the statement in 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 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.

Group D. Step 1 — control of the histories (p.fixed.geometry.one.grid.propagation)

theorem HCPolySupport.HighContrast.Multiscale.meanHistory_nonneg (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 → 0 ≤ meanHistory P γ (Geometry.explicitRoundedGrid jStar metric) n m

The mean history is nonnegative on the admissible range: every Ψ_Q(P^q_{j,m}) is, because the adapted annealed means decrease and normalize above the identity.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_integrable_biSup {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (s : Set ι) (hs : s.Finite) (f : ι → Ω → ℝ) (hf : ∀ (i : ι) (a : Ω), 0 ≤ f i a) (hint : ∀ i ∈ s, MeasureTheory.Integrable (f i) P) : MeasureTheory.Integrable (fun (a : Ω) => ⨆ i ∈ s, f i a) P ∧ ∀ (a : Ω), ∀ i ∈ s, f i a ≤ ⨆ k ∈ s, f k a

Finite nonnegative suprema are integrable and dominate each entry. This supplies the real-supremum justification in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_centers_finite_card {d : ℕ} (q : Mat d) (hq : IsUnit q) (j m : ℤ) (hjm : j ≤ m) : (adaptedLatticeAtScale q j ∩ adaptedCell q m).Finite ∧ (adaptedLatticeAtScale q j ∩ adaptedCell q m).ncard = 3 ^ (d * (m - j).toNat)

Exact centre count in an invertible adapted grid, used to absorb the maximum by a sum in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_centers_decompose {d : ℕ} (q : Mat d) (hq : IsUnit q) (j n m : ℤ) (hjn : j ≤ n) (hnm : n ≤ m) (z : Vec d) (hz : z ∈ adaptedLatticeAtScale q j ∩ adaptedCell q m) : ∃ y ∈ adaptedLatticeAtScale q n ∩ adaptedCell q m, z - y ∈ adaptedLatticeAtScale q j ∩ adaptedCell q n

Compatible centre decomposition through an intermediate generation. The same parent cell is used for every fine scale in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_integral_translate {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (f : CoeffSpace d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f P) (v : Fin d → ℤ) : ∫ (a : CoeffSpace d), f (translateCoeff v a) ∂P = ∫ (a : CoeffSpace d), f a ∂P

Stationarity transports an entire scalar integrand, including its joint supremum. This is the shared-translation step of carried history, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_count_absorption (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (j m : ℤ) (hjm : j ≤ m) : 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑m - ↑j)) * ↑(3 ^ (d * (m - j).toNat)) ≤ 3 ^ (-((1 - γ) / 4) * (↑m - ↑j))

The scale-cell count is absorbed with coefficient one in the decay of carried history, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_normalizedBlock_opNorm_le {d : ℕ} (A F G : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) : blockOpNorm (normalizedBlock A G) ≤ blockOpNorm (normalizedBlock F G) * blockOpNorm (normalizedBlock A F)

Change of normalization in operator norm, without commuting the square roots. This is the matrix congruence in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_integrable_opNorm_pow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (N : ℕ) (hN : 1 ≤ ↑N) (H : CoeffSpace d → BlockMat d) (hmem : SchattenMemLp P (↑N) H) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockOpNorm (H a) ^ N) P

Operator moments are integrable under the existing Schatten membership theorem. This justifies the finite maxima of carried history, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_fluctuation_integrable_dominate (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (metric : Mat d) (hmetric : Matrix.PosDef metric) (k : ℤ) : have q := Geometry.explicitRoundedGrid jStar metric; have f := fun (a : CoeffSpace d) => ⨆ j ∈ Set.Icc (↑jStar) k, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑k - ↑j)) * ⨆ z ∈ adaptedLatticeAtScale q j ∩ adaptedCell q k, blockOpNorm (normalizedFluctuation P q j k z a) ^ bigQ d γ; MeasureTheory.Integrable f P ∧ ∀ (a : CoeffSpace d), ∀ j ∈ Set.Icc (↑jStar) k, ∀ z ∈ adaptedLatticeAtScale q j ∩ adaptedCell q k, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑k - ↑j)) * blockOpNorm (normalizedFluctuation P q j k z a) ^ bigQ d γ ≤ f a

Integrability and pointwise domination for the actual weighted history integrand, as used in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_fluctuation_pow_transport {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (Q : ℕ) (j k l : ℤ) (z : Vec d) (a : CoeffSpace d) (hk : Matrix.PosDef (toFullBlockMat (adaptedMean P q k))) (hl : Matrix.PosDef (toFullBlockMat (adaptedMean P q l))) : blockOpNorm (normalizedFluctuation P q j l z a) ^ Q ≤ blockOpNorm (relMean P q k l) ^ Q * blockOpNorm (normalizedFluctuation P q j k z a) ^ Q

Powered change of normalization for an individual fluctuation. This supplies the matrix factor in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_lattice_moment_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (metric : Mat d) (hmetric : Matrix.PosDef metric) (j m : ℤ) (hj : ↑jStar ≤ j) (hjm : j ≤ m) (z : Vec d) (hz : z ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar metric) j) : have q := Geometry.explicitRoundedGrid jStar metric; ∫ (a : CoeffSpace d), blockOpNorm (normalizedFluctuation P q j m z a) ^ bigQ d γ ∂P ≤ Real.exp (↑(bigQ d γ) * detIncrement P q j m) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P q j a) ^ bigQ d γ ∂P

Stationarity and normalization bound a single fine-cell moment by its diagonal Schatten moment, in the carried-history step, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_integral_sup_split {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (b n m : ℤ) (w : ℤ → ℝ) (hw : ∀ (j : ℤ), 0 < w j) (Z : ℤ → Set ι) (F : ℤ → Finset ι) (f : ℤ → ι → Ω → ℝ) (hf : ∀ (j : ℤ) (z : ι) (a : Ω), 0 ≤ f j z a) (hcover : ∀ j ∈ Finset.Icc (n + 1) m, ∀ z ∈ Z j, z ∈ F j) (hfint : ∀ j ∈ Finset.Icc (n + 1) m, ∀ z ∈ F j, MeasureTheory.Integrable (f j z) P) (L : Ω → ℝ) (hL : ∀ (a : Ω), 0 ≤ L a) (hLint : MeasureTheory.Integrable L P) (hHint : MeasureTheory.Integrable (fun (a : Ω) => ⨆ j ∈ Set.Icc b m, w j * ⨆ z ∈ Z j, f j z a) P) (hlower : ∀ (a : Ω) (j : ℤ), b ≤ j → j ≤ n → ∀ z ∈ Z j, w j * f j z a ≤ L a) : ∫ (a : Ω), ⨆ j ∈ Set.Icc b m, w j * ⨆ z ∈ Z j, f j z a ∂P ≤ ∫ (a : Ω), L a ∂P + ∑ j ∈ Finset.Icc (n + 1) m, ∫ (a : Ω), w j * ∑ z ∈ F j, f j z a ∂P

Split a weighted real supremum at an intermediate generation and replace the upper maxima by finite sums. This is the scalar integration step of carried history, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_fluctuation_pow_le_penalty (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (metric : Mat d) (hmetric : Matrix.PosDef metric) (j n m : ℤ) (hn : ↑jStar ≤ n) (hnm : n ≤ m) (z : Vec d) (a : CoeffSpace d) : have q := Geometry.explicitRoundedGrid jStar metric; blockOpNorm (normalizedFluctuation P q j m z a) ^ bigQ d γ ≤ (1 + meanPenalty (bigQ d γ) (relMean P q n m)) * blockOpNorm (normalizedFluctuation P q j n z a) ^ bigQ d γ

The trace penalty controls the powered normalization factor, for arbitrary fine generation and centre, in carried history, p.fixed.geometry.one.grid.propagation.

theorem HCPolySupport.HighContrast.Multiscale.oneGrid_lower_pointwise (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (metric : Mat d) (hmetric : Matrix.PosDef metric) (n m : ℤ) (hn : ↑jStar ≤ n) (hnm : n ≤ m) (C : Finset (Vec d)) (hC : ↑C = adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar metric) n ∩ adaptedCell (Geometry.explicitRoundedGrid jStar metric) m) (τ : Vec d → Fin d → ℤ) (hτ : ∀ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar metric) n ∩ adaptedCell (Geometry.explicitRoundedGrid jStar metric) m, y = Source.AKL.intTranslation (τ y)) : have q := Geometry.explicitRoundedGrid jStar metric; have H := fun (a : CoeffSpace d) => ⨆ j ∈ Set.Icc (↑jStar) n, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑n - ↑j)) * ⨆ z ∈ adaptedLatticeAtScale q j ∩ adaptedCell q n, blockOpNorm (normalizedFluctuation P q j n z a) ^ bigQ d γ; ∀ (a : CoeffSpace d) (j : ℤ), ↑jStar ≤ j → j ≤ n → ∀ z ∈ adaptedLatticeAtScale q j ∩ adaptedCell q m, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑m - ↑j)) * blockOpNorm (normalizedFluctuation P q j m z a) ^ bigQ d γ ≤ 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑m - ↑n)) * (1 + meanPenalty (bigQ d γ) (relMean P q n m)) * ∑ y ∈ C, H (translateCoeff (τ y) a)

The old-generation bound uses one translated joint supremum per parent cell. This is the compatible partition argument of carried history, p.fixed.geometry.one.grid.propagation.