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

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

Initialization: deterministic scalar, telescoping and block helpers

Deterministic arithmetic used by the initialization route for the fixed-grid scale HCPoly/Entry/Statements/InitialFixedGridScale.lean (p.initial.fixed.grid.scale): logarithm and logb comparisons, the 1 + t ≤ exp t scalar decrement of p.initial.fixed.grid.scale, the good-index extraction of p.initial.fixed.grid.scale, integer telescoping, geometric weight sums, and the block trace and mean-penalty bounds under a Loewner scale bound.

No probability law and no annealed premise enters any statement of this file.

A. Deterministic scalar and matrix helpers

theorem HCPolySupport.HighContrast.Multiscale.ceil_source_threshold_le_of_le (K : ℝ) (hK : 1 < K) (a b : ℝ) (hab : a ≤ b) (j : ℤ) (hb : ⌈b * Real.logb 3 (2 * K)⌉ ≤ j) : ⌈a * Real.logb 3 (2 * K)⌉ ≤ j

A1. The source threshold is monotone in the constant (1 < K gives log₃(2K) ≥ 0).

theorem HCPolySupport.HighContrast.Multiscale.one_le_logb_three_of_three_le (x : ℝ) (hx : 3 ≤ x) : 1 ≤ Real.logb 3 x

A2. log₃(2+Π) ≥ 1 whenever 2+Π ≥ 3 (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.log_aspect_le_logb (Pi : ℝ) (hPi : 1 ≤ Pi) : Real.log (24 * Pi) ≤ (Real.log 24 + Real.log 3) * Real.logb 3 (2 + Pi)

A3. log(24Π) ≤ C log₃(2+Π) with the printed-size constant.

theorem HCPolySupport.HighContrast.Multiscale.half_log_aspect_le (Pi : ℝ) (hPi : 1 ≤ Pi) : 1 / 2 * Real.log (24 * Pi) ≤ Real.log (2 + 4 * Pi)

A4. ½ log(24Π) ≤ log(2+4Π) (the 24Π normalization enters the entry radius).

theorem HCPolySupport.HighContrast.Multiscale.aspect_pow_le_two_add_pow (Pi : ℝ) (hPi : 1 ≤ Pi) (c : ℝ) (hc : 1 ≤ c) (k : ℕ) : (c * Pi) ^ k ≤ c ^ k * (2 + Pi) ^ k

A5. Polynomial bookkeeping in Π: (cΠ)^k ≤ c^k (2+Π)^k.

theorem HCPolySupport.HighContrast.Multiscale.scalar_log_decrement (Q C₀ x x' y : ℝ) (hQ : 0 ≤ Q) (hC₀ : 0 ≤ C₀) (hx : 1 ≤ x) (hy : 0 ≤ y) (hx' : 0 ≤ x') (h : x' ≤ 1 / 8 * Real.exp (Q * y) * x + C₀ * (Real.exp (Q * y) - 1)) : Real.log (1 + x') ≤ Real.log (1 + x) - Real.log (16 / 9) + (Q + 8 / 9 * C₀ * Q) * y

A6. The elementary scalar calculation of p.initial.fixed.grid.scale.

theorem HCPolySupport.HighContrast.Multiscale.exists_good_index_of_decrement (W δ : ℕ → ℝ) (bad : ℕ → Prop) (Ksteps : ℕ) (a c : ℝ) (hW : ∀ (ℓ : ℕ), 0 ≤ W ℓ) (hdec : ∀ ℓ < Ksteps, bad ℓ → W (ℓ + 1) ≤ W ℓ - a + c * δ ℓ) (hK : W 0 + c * ∑ ℓ ∈ Finset.range Ksteps, δ ℓ < ↑Ksteps * a) : ∃ ℓ < Ksteps, ¬bad ℓ

A7. The hitting-index argument of p.initial.fixed.grid.scale, abstractly.

theorem HCPolySupport.HighContrast.Multiscale.sum_Icc_int_telescope (f : ℤ → ℝ) {a b : ℤ} (hab : a ≤ b) : ∑ j ∈ Finset.Icc (a + 1) b, (f (j - 1) - f j) = f a - f b

A8. Integer telescoping over Finset.Icc (a+1) b.

theorem HCPolySupport.HighContrast.Multiscale.geometric_weight_sum_Icc_le (θ : ℝ) (hθ : 0 < θ) (a b : ℤ) : ∑ j ∈ Finset.Icc a b, 3 ^ (-θ * (↑b - ↑j)) ≤ (1 - 3 ^ (-θ))⁻¹

A9. The geometric weight sum over Finset.Icc.

theorem HCPolySupport.HighContrast.Multiscale.geometric_weight_sum_Ico_le (θ : ℝ) (hθ : 0 < θ) (a b : ℤ) : ∑ j ∈ Finset.Ico a b, 3 ^ (-θ * (↑b - 1 - ↑j)) ≤ (1 - 3 ^ (-θ))⁻¹

A10. The geometric weight sum over Finset.Ico, in the mean-history shape.

theorem HCPolySupport.HighContrast.Multiscale.blockPosDef_of_toFullBlockMat_posDef {d : ℕ} (A : BlockMat d) (hA : Matrix.PosDef (toFullBlockMat A)) : Book.Ch02.BlockPosDef A

A12. Positive definiteness of the full matrix gives BlockPosDef (public restatement).

theorem HCPolySupport.HighContrast.Multiscale.blockTrace_sub_identity_le_of_le_scale {d : ℕ} (M : BlockMat d) (c : ℝ) (hM : BlockMatLoewnerLE M (blockScale c (Book.Ch02.blockIdentity d))) : blockTrace (blockSub M (Book.Ch02.blockIdentity d)) ≤ 2 * ↑d * (c - 1)

A13. A block below c·I has tr(M − I) ≤ 2d(c − 1).

theorem HCPolySupport.HighContrast.Multiscale.meanPenalty_le_of_le_scale {d : ℕ} (Q : ℕ) (M : BlockMat d) (hM : IsSymmetricBlockMat M) (c : ℝ) (hc : 1 ≤ c) (hIM : BlockMatLoewnerLE (Book.Ch02.blockIdentity d) M) (hMc : BlockMatLoewnerLE M (blockScale c (Book.Ch02.blockIdentity d))) : meanPenalty Q M ≤ (1 + 2 * ↑d * (c - 1)) ^ Q - 1

A14. The mean penalty of a block I ≤ M ≤ c·I (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.absSchattenNorm_pow_le_of_sandwich {d : ℕ} (Q : ℕ) (hQ : 1 ≤ Q) (H : BlockMat d) (hH : IsSymmetricBlockMat H) (c : ℝ) (hc : 1 ≤ c) (hlo : BlockMatLoewnerLE (blockScale (-1) (Book.Ch02.blockIdentity d)) H) (hhi : BlockMatLoewnerLE H (blockScale c (Book.Ch02.blockIdentity d))) : absSchattenNorm (↑Q) H ^ Q ≤ 2 * ↑d * c ^ Q

A15. The Q-th Schatten moment of a symmetric block sandwiched in [−I, c·I].

theorem HCPolySupport.HighContrast.Multiscale.normalizedBlock_le_scale_and_logDet_le {d : ℕ} (F G : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) (c : ℝ) (hc : 0 < c) (hFG : BlockMatLoewnerLE F (blockScale c G)) : BlockMatLoewnerLE (normalizedBlock F G) (blockScale c (Book.Ch02.blockIdentity d)) ∧ blockLogDet F - blockLogDet G ≤ 2 * ↑d * Real.log c

A16. If F and G are positive definite, 0 < c, and F ≤ c • G in the Loewner order, then normalizedBlock F G ≤ c • I and blockLogDet F - blockLogDet G ≤ 2 d log c.