High-contrast homogenization: Entry.Multiscale.Initial.SourceBounds

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

Initialization: source and normalization bounds on the unrestricted window

HCPoly/Entry/Annealed/ReferenceNormalization.lean carries the initial source and normalization bounds on the window j ≤ 2 j_*. The initialization places its entry generation at n₀ ≥ j_* + ⌈B log₃(2+Π)⌉, unbounded relative to j_*, so both are restated here on the unrestricted range j_* ≤ j ≤ m by re-running the source construction at j in place of j_* (p.initial.fixed.grid.scale). The single-cell sandwich and moment bounds for the normalized self fluctuation at the Euclidean grid follow.

B. Source and normalization bounds on the unrestricted window

(p.initial.fixed.grid.scale, lifting the restriction j ≤ 2 j_*)

theorem HCPolySupport.HighContrast.Multiscale.initial_source_bounds_all (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j : ℤ), ↑jStar ≤ j → BlockMatLoewnerLE (blockScale (1 / 2) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) (adaptedMean P 1 j) ∧ BlockMatLoewnerLE (adaptedMean P 1 j) (blockScale 2 E)

B1. e.initial.source.bounds, first half, for every j ≥ j_*.

theorem HCPolySupport.HighContrast.Multiscale.initial_normalization_bounds_all (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j m : ℤ), ↑jStar ≤ j → j ≤ m → BlockMatLoewnerLE (adaptedMean P 1 m) (adaptedMean P 1 j) ∧ BlockMatLoewnerLE (adaptedMean P 1 j) (blockScale (24 * aspectRatio E) (adaptedMean P 1 m)) ∧ BlockMatLoewnerLE (Book.Ch02.blockIdentity d) (relMean P 1 j m) ∧ BlockMatLoewnerLE (relMean P 1 j m) (blockScale (24 * aspectRatio E) (Book.Ch02.blockIdentity d)) ∧ 0 ≤ detIncrement P 1 j m ∧ detIncrement P 1 j m ≤ 2 * ↑d * Real.log (24 * aspectRatio E)

B2. e.initial.normalization.bounds for every j_* ≤ j ≤ m.

theorem HCPolySupport.HighContrast.Multiscale.coarseBlock_one_source_envelope (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j : ℤ), ↑jStar ≤ j → ∃ (X : CoeffSpace d → ℝ), Measurable X ∧ (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => X a ^ bigQ d γ) P ∧ ∫ (a : CoeffSpace d), X a ^ bigQ d γ ∂P ≤ 2 ^ bigQ d γ ∧ ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (adaptedCell 1 j) a) (blockScale (X a) E)

B3. The source envelope of the Euclidean scale-j cell, j ≥ j_* (e.source.adapted.bound at the window j, standard-cube clause).

theorem HCPolySupport.HighContrast.Multiscale.normalizedFluctuationSelf_one_sandwich (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j : ℤ), ↑jStar ≤ j → ∀ (a : CoeffSpace d) (X : ℝ), 0 ≤ X → BlockMatLoewnerLE (coarseBlock (adaptedCell 1 j) a) (blockScale X E) → BlockMatLoewnerLE (blockScale (-1) (Book.Ch02.blockIdentity d)) (normalizedFluctuationSelf P 1 j a) ∧ BlockMatLoewnerLE (normalizedFluctuationSelf P 1 j a) (blockScale (12 * aspectRatio E * X) (Book.Ch02.blockIdentity d))

B4 (kernel). The pathwise sandwich −I ≤ V^Id_j ≤ 12Π X·I of the self-normalized fluctuation, from the envelope and 𝐄 ≤ 6Π𝐑𝐄⁻¹𝐑 ≤ 12Π 𝐀hom_{j,Id}.

theorem HCPolySupport.HighContrast.Multiscale.normalizedFluctuationSelf_one_moment_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j : ℤ), ↑jStar ≤ j → ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P 1 j a) ^ bigQ d γ ∂P ≤ 2 * ↑d * (1 + (24 * aspectRatio E) ^ bigQ d γ)

B5 (kernel). e.initial.source.bounds, second half: E|V^Id_j|^Q_{S_Q} ≤ (CΠ)^Q.

theorem HCPolySupport.HighContrast.Multiscale.fluctuationHistory_one_jStar_le_moment (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → fluctuationHistory P γ 1 jStar ↑jStar ≤ ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P 1 (↑jStar) a) ^ bigQ d γ ∂P

B6 (kernel). The seed: the Euclidean fluctuation history at j_* is the single-cell moment (adaptedLatticeAtScale 1 j_* ∩ adaptedCell 1 j_* = {0}, both cells open).