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

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

Tail exponents for the quenched minimal scale

This file isolates the real-variable exponent used in the corrected finite sigma theorem. The mixed bottom range optimizes a Gamma_tau localized tail against a Gamma_sigma crude tail; the resulting exponent is the interpolated one recorded below.

def HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailTau (σ : ℝ) : ℝ

The finite-sigma concentration exponent after the Chapter 4 concentration step.

Equations

• HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailTau σ = min σ 2

noncomputable def HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent (b σ t : ℝ) : ℝ

The corrected finite-sigma exponent for Theorem t.homogenization.quenched, written with an abstract b = d / 2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent (d : ℕ) (σ t : ℝ) : ℝ

Dimension-specialized version of interpolatedQuenchedTailExponent.

Equations

• HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent d σ t = HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent (↑d / 2) σ t

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailTau_pos {σ : ℝ} (hσ : 0 < σ) : 0 < finiteQuenchedTailTau σ

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailDen_pos {b σ t : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) : 0 < σ * t + finiteQuenchedTailTau σ * (b - t)

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_pos {b σ t : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) : 0 < interpolatedQuenchedTailExponent b σ t

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent_pos {d : ℕ} [NeZero d] {σ t : ℝ} (hσ : 0 < σ) (ht : 0 < t) : 0 < finiteQuenchedTailExponent d σ t

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_le_tau_mul_b {b σ t : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) (htb : t ≤ b) : interpolatedQuenchedTailExponent b σ t ≤ finiteQuenchedTailTau σ * b

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_le_sigma_mul_t {b σ t : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) : interpolatedQuenchedTailExponent b σ t ≤ σ * t

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_le_mixed {b σ t : ℝ} : interpolatedQuenchedTailExponent b σ t ≤ σ * finiteQuenchedTailTau σ * b * t / (σ * t + finiteQuenchedTailTau σ * (b - t))

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_mul_le_max_mixed {b σ t q j : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) (htb : t ≤ b) (hj : 0 ≤ j) (hjq : j ≤ q) : have τ := finiteQuenchedTailTau σ; have η := interpolatedQuenchedTailExponent b σ t; η * q ≤ max (τ * (b * q - (b - t) * j)) (σ * t * j)

The mixed bottom exponent collapse.

In the bottom range, write j = q - n. The localized tail contributes tau * (b*q - (b-t)*j) and the crude tail contributes sigma*t*j. Their maximum dominates the corrected finite exponent times q.

theorem HCPolySupport.Book.Ch05.Section57.interpolatedQuenchedTailExponent_mul_add_row_le_max_mixed {b σ t α q j r : ℝ} (hb : 0 < b) (hσ : 0 < σ) (ht : 0 < t) (hαt : α < t) (htb : t ≤ b) (hj : 0 ≤ j) (hjq : j ≤ q) (hr : 0 ≤ r) : have τ := finiteQuenchedTailTau σ; have η := interpolatedQuenchedTailExponent b σ t; η * q + τ * (t - α) * r ≤ max (τ * (b * q - (b - t) * j + (t - α) * r)) (σ * (t * j + (t - α) * r))

Mixed bottom collapse with the row gain retained. The row variable r is the distance above the bad scale; since both stochastic mechanisms gain (t - alpha) * r, the maximum retains a positive weighted-kernel gain.

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent_mul_nat_le_tau_mul_b_nat {d : ℕ} [NeZero d] {σ t : ℝ} {q : ℕ} (hσ : 0 < σ) (ht : 0 < t) (htb : t ≤ ↑d / 2) : finiteQuenchedTailExponent d σ t * ↑q ≤ finiteQuenchedTailTau σ * (↑d / 2) * ↑q

Dimension-specialized high-top collapse: the finite bad-scale exponent is no larger than the localized tau * d/2 exponent.

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent_mul_nat_le_sigma_mul_t_nat {d : ℕ} [NeZero d] {σ t : ℝ} {q : ℕ} (hσ : 0 < σ) (ht : 0 < t) : finiteQuenchedTailExponent d σ t * ↑q ≤ σ * t * ↑q

Dimension-specialized crude-bottom collapse: the finite bad-scale exponent is no larger than the crude sigma * t exponent.

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent_mul_nat_le_max_bottom {d q n : ℕ} [NeZero d] {σ t : ℝ} (hσ : 0 < σ) (ht : 0 < t) (htb : t ≤ ↑d / 2) : have b := ↑d / 2; have τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have j := ↑(q - n); η * ↑q ≤ max (τ * (b * ↑q - (b - t) * j)) (σ * t * j)

Dimension-specialized mixed-bottom collapse in shifted natural indices. Here j = q - n is the distance from the bad scale down to the bottom scale.

theorem HCPolySupport.Book.Ch05.Section57.finiteQuenchedTailExponent_mul_nat_add_row_le_max_bottom {d q n r : ℕ} [NeZero d] {σ t α : ℝ} (hσ : 0 < σ) (ht : 0 < t) (hαt : α < t) (htb : t ≤ ↑d / 2) : have b := ↑d / 2; have τ := finiteQuenchedTailTau σ; have η := finiteQuenchedTailExponent d σ t; have j := ↑(q - n); η * ↑q + τ * (t - α) * ↑r ≤ max (τ * (b * ↑q - (b - t) * j + (t - α) * ↑r)) (σ * (t * j + (t - α) * ↑r))

Dimension-specialized mixed-bottom collapse with the row gain retained.