High-contrast homogenization: Entry.Source.BoundedWindowFiniteness

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

Bounded-window source moments

p.fixed.geometry.parent.child.recurrence, plan B4. The auxiliary source window is separate from the consumer's fixed rounded grid. Each finite real exponent uses a fresh sufficiently high source moment. Only finiteness is asserted; the fixed-Q uniform bound is not reused.

theorem HCPolySupport.HighContrast.Source.source_minimum_memLp_all {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jWindow : ℕ) (ell : CoeffSpace d → ℕ) (X : CoeffSpace d → ℝ) (hell : Measurable ell) (hX : Measurable X) (hform : ∀ (a : CoeffSpace d), X a = 3 ^ (γ * ↑(ell a))) (htail : ∀ (p : ℝ), 1 ≤ p → ∀ (r : ℕ), P.real {a : CoeffSpace d | r < ell a} ≤ (3 ^ (d * jWindow) * ∫ (a : CoeffSpace d), S a ^ p ∂P) / (3 ^ (jWindow + r)) ^ p) (N : ℝ) : 1 ≤ N → MeasureTheory.MemLp X (ENNReal.ofReal N) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => X a ^ N) P

Every finite moment of a characterized source minimum exists on any fixed auxiliary window. This repeats the tail argument with a new source moment and asserts no uniform norm bound at the new exponent. The consumer's rounded grid is not changed.

theorem HCPolySupport.HighContrast.Source.source_minimum_all_moments {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) (jWindow : ℕ) : have Good := fun (r : ℕ) (a : CoeffSpace d) => ∀ (w : Fin d → ℤ), standardCellCenter (↑(jWindow + r)) w ∈ centeredCube d ↑(2 * jWindow + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jWindow + r) * w i) a) ≤ 3 ^ (jWindow + r); ∃ (ell : CoeffSpace d → ℕ) (X : CoeffSpace d → ℝ), Measurable ell ∧ Measurable X ∧ (∀ (a : CoeffSpace d), X a = 3 ^ (γ * ↑(ell a))) ∧ (∀ (a : CoeffSpace d), (¬∃ (r : ℕ), Good r a) → ell a = 0) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, Good (ell a) a ∧ (∀ (r : ℕ), Good r a → ell a ≤ r) ∧ ∀ (r : ℕ), Good r a → X a ≤ 3 ^ (γ * ↑r)) ∧ (γ = 0 → ∀ (a : CoeffSpace d), X a = 1) ∧ ∀ (N : ℝ), 1 ≤ N → MeasureTheory.MemLp X (ENNReal.ofReal N) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => X a ^ N) P

On any auxiliary source window the attained minimum has every finite moment. No source threshold or change to a consumer's rounded metric is required.

theorem HCPolySupport.HighContrast.Source.exists_auxiliary_source_window {d : ℕ} {W : Set (Vec d)} (hW : Bornology.IsBounded W) : ∃ (J : ℕ), W ⊆ centeredCube d (2 * ↑J)

Every bounded region fits in an auxiliary centered source window. The window is independent of a consumer's fixed rounded grid and of any source threshold.

theorem HCPolySupport.HighContrast.Source.bounded_source_envelope {d : ℕ} [NeZero 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) (W : Set (Vec d)) (hW : Bornology.IsBounded W) : ∃ (J : ℕ) (X : CoeffSpace d → ℝ), Measurable X ∧ (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ (∀ (N : ℝ), 1 ≤ N → MeasureTheory.MemLp X (ENNReal.ofReal N) P) ∧ ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (q : Mat d), Geometry.InverseNormLE q 2 → ∀ (j : ℤ) (y : Vec d), adaptedCellTranslate q j y ⊆ W → BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate q j y) a) (blockScale (12 * ↑d ^ (3 / 2) / (1 - 3 ^ (-(1 - γ))) * X a * 3 ^ (γ * max (↑J - ↑j) 0)) E)

A bounded region has one measurable source envelope with every finite real moment, simultaneously for all adapted cells with the rounded inverse bound. The auxiliary scale is proof data and asserts no uniform norm bound.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_of_order_envelope {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {A : CoeffSpace d → BlockMat d} {E : BlockMat d} (hAm : HasMeasurableBlock P A) (hAs : ∀ᵐ (a : CoeffSpace d) ∂P, IsSymmetricBlockMat (A a)) (hAp : ∀ᵐ (a : CoeffSpace d) ∂P, Book.Ch02.BlockPosDef (A a)) {X : CoeffSpace d → ℝ} (hX : MeasureTheory.MemLp X (ENNReal.ofReal N) P) (D : ℝ) (horder : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (A a) (blockScale (D * X a) E)) : SchattenMemLp P N A

An integrable scalar order envelope supplies Schatten membership after measurability and full spectral positivity have been established.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_coarseBlock_adapted (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 : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (y : Vec d) (N : ℝ) (hN : 1 ≤ N) : SchattenMemLp P N fun (a : CoeffSpace d) => coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) a

Bounded-window generalized finiteness for every finite real moment. The proof chooses its own auxiliary source window and moment; it needs neither the original source containment nor its fixed-Q threshold, and gives no new uniform norm bound.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_congruence {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {A : CoeffSpace d → BlockMat d} (hA : SchattenMemLp P N A) (hN : 1 ≤ N) (B : FullBlockMat d) : SchattenMemLp P N fun (a : CoeffSpace d) => ofFullBlockMat (Matrix.conjTranspose B * toFullBlockMat (A a) * B)

Deterministic full-matrix congruence preserves finite Schatten membership. No annealed identity or positivity normalization is used.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_normalizedBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {A : CoeffSpace d → BlockMat d} (hA : SchattenMemLp P N A) (hN : 1 ≤ N) (R : BlockMat d) : SchattenMemLp P N fun (a : CoeffSpace d) => normalizedBlock (A a) R

The deterministic inverse-square-root normalization preserves membership. The root's total definition is symmetric even at its junk branch; a source consumer may in particular take any positive reference block R.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_finset_sum {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) (s : Finset ι) (w : ι → ℝ) (A : ι → CoeffSpace d → BlockMat d) (hA : ∀ i ∈ s, SchattenMemLp P N (A i)) : SchattenMemLp P N fun (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ s, w i • toFullBlockMat (A i a))

Every deterministic finite weighted sum of Schatten members is a member. The empty family is included, and the dimension factor proves finiteness only.

theorem HCPolySupport.HighContrast.Source.annealedBlock_adapted_add_intTranslation {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (z : Fin d → ℤ) : annealedBlock P (adaptedCellTranslate q j (y + Source.AKL.intTranslation z)) = annealedBlock P (adaptedCellTranslate q j y)

S2 integer stationarity identifies the actual entrywise annealed means. This uses only measurable transport and does not assume annealed normalization.