Uniform scale-normalized bounds for the auxiliary diffusivity chain.

theorem AVenhance.Infra.Section3.KappaPrimeUniform.epsilon_le_128_rpow_neg {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : epsilon β Λ m ≤ 128 ^ (-↑m)

theorem AVenhance.Infra.Section3.KappaPrimeUniform.finite_geometric_sum_le {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (n : ℕ) : ∑ i ∈ Finset.range n, r ^ i ≤ 1 / (1 - r)

theorem AVenhance.Infra.Section3.KappaPrimeUniform.rpow_neg_nat_eq_inv_pow {x : ℝ} (hx : 0 < x) (n : ℕ) : x ^ (-↑n) = x⁻¹ ^ n

theorem AVenhance.Infra.Section3.KappaPrimeUniform.rpow_neg_nat_mul_eq_pow {x p : ℝ} (hx : 0 < x) (n : ℕ) : x ^ (-↑n * p) = (x ^ (-p)) ^ n

noncomputable def AVenhance.Infra.Section3.kappaPrimeRatioError (β : ℝ) : ℝ

The β-dependent linear error coefficient for one normalized scale ratio.

Equations

• AVenhance.Infra.Section3.kappaPrimeRatioError β = 2 * AVenhance.Infra.Ingredients.supergeoConstant β + AVenhance.Infra.Ingredients.supergeoConstant β ^ 2 / 128

noncomputable def AVenhance.Infra.Section3.kappaPrimeEndpointConstant (β : ℝ) : ℝ

Uniform bound immediately below the permitted terminal scale.

Equations

• AVenhance.Infra.Section3.kappaPrimeEndpointConstant β = max ((1 + AVenhance.Infra.Section3.kappaPrimeRatioError β / 128) * (2 + 2 * (9 / 80))) ((1 + 50 / 128) * (2 * (9 / 80)))

noncomputable def AVenhance.Infra.Section3.kappaPrimeUniformConstant (β : ℝ) : ℝ

A β-only bound for every reciprocal-symmetric normalized κ′ value.

Equations

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

theorem AVenhance.Infra.Section3.KappaPrimeUniform.kappaPrimeNormalized_terminal_bounds {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (_hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) : 1 / 2 * epsilon β Λ M ^ (-2 * gamma β) ≤ kappaPrimeNormalized β Λ κ M 0 ∧ kappaPrimeNormalized β Λ κ M 0 ≤ 2 * epsilon β Λ M ^ (-2 * gamma β)

theorem AVenhance.Infra.Section3.KappaPrimeUniform.kappaPrimeNormalizedSize_endpoint_bound {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ (m + 1)) (hm : 1 ≤ m) : kappaPrimeNormalizedSize β Λ κ m 1 ≤ kappaPrimeEndpointConstant β

The last normalized recurrence step cancels the scale-dependent size of the permitted terminal value.

theorem AVenhance.Infra.Section3.KappaPrimeUniform.kappaPrimeNormalizedSize_chain_bound_to {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (m d r : ℕ) : kappaPrimeNormalizedSize β Λ κ m (d + r) ≤ (∏ i ∈ Finset.range d, kappaPrimeNormalizedStepFactor β Λ (m + i)) * kappaPrimeNormalizedSize β Λ κ (m + d) r

Iterate the size recurrence for a chosen number of steps, leaving a positive depth at the endpoint.

theorem AVenhance.Infra.Section3.KappaPrimeUniform.kappaPrimeNormalizedStepFactor_bound {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : kappaPrimeNormalizedStepFactor β Λ m ≤ (1 + max (kappaPrimeRatioError β) 50 * epsilon β Λ m) * (1 + epsilon β Λ (m + 1) ^ (2 * gamma β))

theorem AVenhance.Infra.Section3.KappaPrimeUniform.kappaPrimeNormalizedStepFactor_product_bound {β : ℝ} {Λ m d : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : ∏ i ∈ Finset.range d, kappaPrimeNormalizedStepFactor β Λ (m + i) ≤ Real.exp (max (kappaPrimeRatioError β) 50 * (128 / 127) + 1 / (1 - 128 ^ (-2 * gamma β)))

theorem AVenhance.Infra.Section3.kappaPrimeNormalizedSize_uniform_bound {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) {m : ℕ} (hm : 1 ≤ m) (hmM : m < M) : kappaPrimeNormalizedSize β Λ κ m (M - m) ≤ kappaPrimeUniformConstant β

The reciprocal-symmetric normalized auxiliary chain has a uniform β-dependent bound at every scale 1 ≤ m < M with a permitted terminal value.

theorem AVenhance.Infra.Section3.kappaPrimeAt_uniform_bounds {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) {m : ℕ} (hm : 1 ≤ m) (hmM : m < M) : 9 / 80 / kappaPrimeUniformConstant β * (a β Λ m * epsilon β Λ m ^ (2 + gamma β)) ≤ kappaPrimeAt β Λ κ m (M - m) ∧ kappaPrimeAt β Λ κ m (M - m) ≤ kappaPrimeUniformConstant β * (a β Λ m * epsilon β Λ m ^ (2 + gamma β))

The auxiliary sequence satisfies two-sided uniform scale bounds on the corrected range 1 ≤ m < M. The scale is a_m ε_m^(2+γ).