High-contrast homogenization: Entry.Annealed.ShortBridge

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

The successful short bridge on rounded grids

Ordinary support for p.successful.short.bridge. The actual profile and histories retain their definitions. Their finite suprema and moments are justified before the profile is used. Constants are selected before the law in the printed order.

S5 is consumed transitively at , as documented in BridgeSourceTail.

theorem HCPolySupport.HighContrast.Annealed.bridge_fluctuation_memLqSchatten (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 k : ℤ) (z : Vec d) : SchattenMemLp P (↑(bigQ d γ)) (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) j k z)

All translated normalized fluctuations have the actual finite moments used in both the profile and its history. This invokes bounded-window finiteness, without imposing the original source window on auxiliary cells.

theorem HCPolySupport.HighContrast.Annealed.bridge_fluctuationHistory_integrable (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) (k : ℤ) (hk : ↑jStar ≤ k) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => ⨆ j ∈ Set.Icc (↑jStar) k, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑k - ↑j)) * ⨆ z ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j ∩ adaptedCell (Geometry.explicitRoundedGrid jStar m) k, blockOpNorm (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) j k z a) ^ bigQ d γ) P ∧ 0 ≤ fluctuationHistory P γ (Geometry.explicitRoundedGrid jStar m) jStar k

The history's two real suprema are finite, attained maxima on nonempty families, and its defining random variable is integrable. In particular its expectation is nonnegative for its intended reason.

theorem HCPolySupport.HighContrast.Annealed.bridge_profile_nonneg (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) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) : 0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n

Nonnegativity of the actual complete profile, with all its random moments and history suprema justified by the preceding receipts.

theorem HCPolySupport.HighContrast.Annealed.bridge_source_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (Pi c₀ B₀ : ℝ), 1 ≤ Pi → 0 < c₀ → ∀ (L : ℕ), 1 ≤ L → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → projectiveDistance m mPlus ≤ 1 → ∀ (jStar k n : ℤ), jStar ≤ k → k ≤ n → Real.log (‖m‖ * ‖m⁻¹‖) ≤ c₀ / ↑L * (↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + Pi)⌉) → (1 + Pi * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * (1 + ↑n + ↑L - ↑jStar) * 3 ^ (-((1 - γ) / 8) * (↑n - ↑jStar)) ≤ C * (1 + ↑L) * (2 + Pi) ^ (1 - (1 - γ) * B₀ / 16) * Real.exp (-(↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + Pi)⌉) * ((1 - γ) * Real.log 3 / 16 - 2 * c₀ / ↑L))

The printed source bound, including its bracket-dependent exponential. Its explicit constant depends only on gamma; both real-power bases are positive before they are converted to exponentials.

theorem HCPolySupport.HighContrast.Annealed.bridge_length_decay (L₀ L : ℕ) (σ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) (hL : ↑L₀ + ⌈Real.logb 3 σ⁻¹⌉ ≤ ↑L) : L₀ ≤ L ∧ 3 ^ (-↑L) ≤ 3 ^ (-↑L₀) * σ

The ceiling in the length hypothesis supplies precisely the factor sigma.

theorem HCPolySupport.HighContrast.Annealed.bridge_choose_source_separation (γ C : ℝ) (hγ : γ ∈ Set.Ico 0 1) (hC : 0 < C) (σ : ℝ) (hσ : 0 < σ) (L : ℕ) : ∃ (B₀ : ℝ), 1 ≤ B₀ ∧ ∀ (Pi : ℝ), 1 ≤ Pi → C * (1 + ↑L) * (2 + Pi) ^ (1 - (1 - γ) * B₀ / 16) ≤ σ / 3

A logarithm and ceiling choose B0 before Pi, uniformly for all Pi at least one. Thus this choice precedes the coefficient law and reference block.

theorem HCPolySupport.HighContrast.Annealed.bridge_preliminary_comparison (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (K₀ : ℝ) (Csrc : ℝ) (C : ℝ), 1 ≤ K₀ ∧ 0 < Csrc ∧ 0 < C ∧ ∀ c₀ ∈ Set.Ioo 0 1, ∀ σ ∈ Set.Ioc 0 1, ∀ (L : ℕ), 1 ≤ L → 2 * c₀ / ↑L ≤ (1 - γ) * Real.log 3 / 16 → ∀ (B₀ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → Real.log (‖m‖ * ‖m⁻¹‖) ≤ c₀ / ↑L * (↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + aspectRatio E)⌉) → projectiveDistance m mPlus ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n + detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L) ≤ c₀ * σ → blockOpNorm (blockSub (normalizedBlock (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) (Book.Ch02.blockIdentity d)) ≤ C * c₀ * σ + C * K₀ * 3 ^ (-↑L) + C * (1 + ↑L) * (2 + aspectRatio E) ^ (1 - (1 - γ) * B₀ / 16)

The preliminary normalized short-bridge comparison. The displayed lower bound on length is discharged by the ordered constant choice in the endpoint.

theorem HCPolySupport.HighContrast.Annealed.successful_short_bridge_roundedGrid (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (L₀ : ℕ), ∃ c₀ ∈ Set.Ioo 0 1, ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ σ ∈ Set.Ioc 0 1, ∀ (L : ℕ), ↑L₀ + ⌈Real.logb 3 σ⁻¹⌉ ≤ ↑L → ∃ (B₀ : ℝ), 1 ≤ B₀ ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → Real.log (‖m‖ * ‖m⁻¹‖) ≤ c₀ / ↑L * (↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + aspectRatio E)⌉) → k + 2 * ↑(bigQ d γ) ≤ n → projectiveDistance m mPlus ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n + detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L) ≤ c₀ * σ → BlockMatLoewnerLE (blockScale (1 - σ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) ∧ BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (blockScale (1 + σ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L)))

The ordinary rounded-grid endpoint with all stochastic, source, and normalization obligations discharged. The unit-range and separation premises retain their positions.