Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ExponentCompetition

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

Exponent competition for the quenched minimal scale

This file contains the deterministic real-variable inequalities behind the "on top of the exponent" step in Theorem t.homogenization.quenched.

theorem HCPolySupport.Book.Ch05.Section57.natCeil_le_add_max_zero_add_one {L y : ℝ} (hL : 0 ≤ L) : ↑⌈L + y⌉₊ ≤ L + max y 0 + 1

theorem HCPolySupport.Book.Ch05.Section57.highExponentCompetitionConst_pos {a b t α : ℝ} (ha : 0 < a) (hb : 0 < b) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) : 0 < min b (min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))))

theorem HCPolySupport.Book.Ch05.Section57.highSharpExponentCompetitionConst_pos {a b t α : ℝ} (ha : 0 < a) (hb : 0 < b) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) : 0 < min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a))))

theorem HCPolySupport.Book.Ch05.Section57.exists_alpha_for_highCompetition {a b t : ℝ} (ha : 0 < a) (hb : 0 < b) (ht : 0 < t) : ∃ (α : ℝ), 0 < α ∧ α < t ∧ α < a ∧ α < b ∧ α * (1 + b / a) < b

theorem HCPolySupport.Book.Ch05.Section57.highExponentCompetition_lower_bound {a b t α L q r j : ℝ} (ha : 0 < a) (hb : 0 < b) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) (_hL : 0 ≤ L) (hq : 0 ≤ q) (hr : 0 ≤ r) (hj : 0 ≤ j) (hjr : j ≤ r) : have x := (α - t) * r + t * j; have c := min b (min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a))))); b * (q + j) - b * (L + max (x / a) 0 + 1) - x ≥ c * (q + r) - b * (L + 1)

Core real-variable exponent competition in the high range q ≤ n.

The variables are r = m - q and j = n - q, so 0 ≤ j ≤ r. The term L + max (x/a) 0 + 1 is the ceiling upper bound for the intermediate scale, where x = α r - t (r - j) = (α - t)r + t j.

theorem HCPolySupport.Book.Ch05.Section57.highNatScaleExponent_lower_bound_of_ceil {a b t α L : ℝ} {q m n ℓ : ℕ} (ha : 0 < a) (hb : 0 < b) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) (hL : 0 ≤ L) (hℓn : ℓ ≤ n) (hqn : q ≤ n) (hnm : n ≤ m) (hceil : have x := α * ↑(m - q) - t * ↑(m - n); ↑ℓ ≤ L + max (x / a) 0 + 1) : have x := α * ↑(m - q) - t * ↑(m - n); have c := min b (min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a))))); b * ↑(n - ℓ) - x ≥ c * (↑q + ↑(m - q)) - b * (L + 1)

Integer-scale version of highExponentCompetition_lower_bound.

This is the form used for high bad pairs, where the bad scale q is below the localized scale n.

theorem HCPolySupport.Book.Ch05.Section57.highExponentCompetition_lower_bound_sharp {a b t α L q r j : ℝ} (ha : 0 < a) (_hb : 0 < b) (_hαt : α < t) (_hαb : α < b) (_hαharm : α * (1 + b / a) < b) (_hL : 0 ≤ L) (hr : 0 ≤ r) (hj : 0 ≤ j) (hjr : j ≤ r) : have x := (α - t) * r + t * j; have c := min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))); b * (q + j) - b * (L + max (x / a) 0 + 1) - x ≥ b * q + c * r - b * (L + 1)

Sharp high-range exponent competition when the bad scale is below the localized scale. This keeps the manuscript's b q concentration gain.

theorem HCPolySupport.Book.Ch05.Section57.highNatScaleExponent_lower_bound_of_ceil_q_le_n_sharp {a b t α L : ℝ} {q m n ℓ : ℕ} (ha : 0 < a) (hb : 0 < b) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) (hL : 0 ≤ L) (hℓn : ℓ ≤ n) (hqn : q ≤ n) (hnm : n ≤ m) (hceil : have x := α * ↑(m - q) - t * ↑(m - n); ↑ℓ ≤ L + max (x / a) 0 + 1) : have x := α * ↑(m - q) - t * ↑(m - n); have c := min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))); b * ↑(n - ℓ) - x ≥ b * ↑q + c * ↑(m - q) - b * (L + 1)

Integer-scale sharp high-range exponent competition in the case q ≤ n.

theorem HCPolySupport.Book.Ch05.Section57.highNatScaleExponent_lower_bound_of_ceil_any_q {a b t α L : ℝ} {q m n ℓ : ℕ} (ha : 0 < a) (hb : 0 < b) (ht : 0 < t) (hαt : α < t) (hαb : α < b) (hαharm : α * (1 + b / a) < b) (hL : 0 ≤ L) (hℓn : ℓ ≤ n) (hqm : q ≤ m) (hnm : n ≤ m) (hceil : have x := α * ↑(m - q) - t * ↑(m - n); ↑ℓ ≤ L + max (x / a) 0 + 1) : have x := α * ↑(m - q) - t * ↑(m - n); have c := min t (min b (min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))))); b * ↑(n - ℓ) - x ≥ c * (↑q + ↑(m - q)) - b * (L + 1)

High-scale exponent competition without assuming that the bad scale lies below the localized scale. If q ≤ n, this is the previous bridge with a slightly smaller constant; if n < q, the post-discount exponent itself gives the missing decay in q - n.

theorem HCPolySupport.Book.Ch05.Section57.n_le_logOffset_add_one_of_not_high_x_nonpos {a L x : ℝ} {n ℓ : ℕ} (hceil : ↑ℓ ≤ L + max (x / a) 0 + 1) (hx : x / a ≤ 0) (hnℓ : n ≤ ℓ) : ↑n ≤ L + 1

If the selected high scale is not below n and the exponent correction is nonpositive, then n is bounded by the deterministic logarithmic offset.

theorem HCPolySupport.Book.Ch05.Section57.scale_bound_of_not_high_x_le_alpha_mul_n {a α L x : ℝ} {n ℓ : ℕ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (_hαa : α < a) (hceil : ↑ℓ ≤ L + max (x / a) 0 + 1) (hx : x ≤ α * ↑n) (hnℓ : n ≤ ℓ) : (1 - α / a) * ↑n ≤ L + 1

If the selected high scale is not below n, and the exponent correction is at most α n with α < a, then n is bounded by the deterministic logarithmic offset with buffer 1 - α/a.

theorem HCPolySupport.Book.Ch05.Section57.highComplement_x_div_nonpos_of_n_le_q {a t α : ℝ} {q m n : ℕ} (ha : 0 < a) (ht : 0 < t) (hαt : α < t) (hnq : n ≤ q) (hqm : q ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); x / a ≤ 0

In the complementary high-scale range with n ≤ q, the exponent correction is nonpositive.

theorem HCPolySupport.Book.Ch05.Section57.highComplement_x_le_alpha_mul_n_of_q_le_n {t α : ℝ} {q m n : ℕ} (hα_nonneg : 0 ≤ α) (hαt : α < t) (hqn : q ≤ n) (hnm : n ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); x ≤ α * ↑n

In the complementary high-scale range with q ≤ n, the exponent correction is at most α n.

theorem HCPolySupport.Book.Ch05.Section57.n_le_logOffset_add_one_of_not_high_n_le_q {a t α L : ℝ} {q m n ℓ : ℕ} (ha : 0 < a) (ht : 0 < t) (hαt : α < t) (hceil : have x := α * ↑(m - q) - t * ↑(m - n); ↑ℓ ≤ L + max (x / a) 0 + 1) (hnℓ : n ≤ ℓ) (hnq : n ≤ q) (hqm : q ≤ m) : ↑n ≤ L + 1

If the selected high scale is not below n and n ≤ q, then n is bounded by the logarithmic offset.

theorem HCPolySupport.Book.Ch05.Section57.scale_bound_of_not_high_q_le_n {a t α L : ℝ} {q m n ℓ : ℕ} (ha : 0 < a) (hα_nonneg : 0 ≤ α) (hαt : α < t) (hαa : α < a) (hceil : have x := α * ↑(m - q) - t * ↑(m - n); ↑ℓ ≤ L + max (x / a) 0 + 1) (hnℓ : n ≤ ℓ) (hqn : q ≤ n) (hnm : n ≤ m) : (1 - α / a) * ↑n ≤ L + 1

If the selected high scale is not below n and q ≤ n, then n is bounded by the logarithmic offset with the buffer 1 - α/a.

theorem HCPolySupport.Book.Ch05.Section57.crudeBottomExponent_lower_bound {t α : ℝ} {q m n : ℕ} (hnq : n ≤ q) (hqm : q ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); have c := min (t - α) t; -x ≥ c * (↑(m - q) + ↑(q - n))

Bottom-range exponent competition for the crude estimate. Here r = m - q and j = q - n, so the discount gives decay in both directions.

theorem HCPolySupport.Book.Ch05.Section57.crudeTopExponent_lower_bound_of_q_le_n {t α c : ℝ} {q m n : ℕ} (hα_nonneg : 0 ≤ α) (hc_le : c ≤ t - α) (hqn : q ≤ n) (hnm : n ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); -x ≥ c * ↑(m - n) - α * ↑n

Crude exponent competition in the range q ≤ n. The price is an α n offset, which is harmless once the complementary high-scale argument has bounded n.