Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.IterationConstants

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Constant selection for the small-contrast algebraic iteration

def HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.threeQuarterScale (m : ℕ) : ℕ

The lower scale used in the nonlinear iteration.

Equations

• HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.threeQuarterScale m = m - m / 4

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.threeQuarterScale_lt_self {m : ℕ} (hm : 4 ≤ m) : threeQuarterScale m < m

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.half_le_two_threeQuarterScale_sub (m : ℕ) : m / 2 ≤ 2 * threeQuarterScale m - m

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.threeQuarterScale_decay_sq_le {α : ℝ} (hα_nonneg : 0 ≤ α) (m : ℕ) : Real.rpow 3 (-α * ↑(threeQuarterScale m)) ^ 2 ≤ Real.rpow 3 (-α * ↑m) * Real.rpow 3 (-α * ↑(m / 2))

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.lagged_scale_window {L m : ℕ} (hL_pos : 0 < L) (hlarge : 8 * L + 4 ≤ m) : threeQuarterScale m < m - L ∧ m - L < m ∧ L ≤ m - (m - L) ∧ m / 8 ≤ m - L - threeQuarterScale m

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.scale_div_sixteen_le_nat_div_eight_cast {m : ℕ} (hm : 16 ≤ m) : ↑m / 16 ≤ ↑(m / 8)

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.exists_decay_rate_for_lag_contraction {L : ℕ} {θ α0 : ℝ} (hL_pos : 0 < L) (hθ_pos : 0 < θ) (hθ_lt_one : θ < 1) (hα0_pos : 0 < α0) : ∃ (α : ℝ), 0 < α ∧ α ≤ α0 ∧ θ * Real.rpow 3 (α * ↑L) < 1

There is a positive exponential rate compatible with a fixed contraction and lag.