Bootstrap estimates comparing the diffusivity recursion with κ′.

The top endpoint is treated directly from the permitted interval. Interior steps use the corrected κ′ exprat estimate and the unconditional averaging bound.

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

The top permitted value also has a small exprat ratio, with the 2δ exponent.

Equations

• AVenhance.Infra.Section3.kappaPrimeEndpointExpratConstant β = 2 ^ 34 * (1 + AVenhance.Infra.Ingredients.supergeoConstant β / 128) ^ (2 - β + AVenhance.gamma β)

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.endpoint_exponent_gap {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 * delta β ≤ q β * (2 - β + gamma β) - (2 - β + 4 * delta β)

theorem AVenhance.Infra.Section3.kappaPrimeAt_terminal_exprat_upper {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) (hM : 2 ≤ M) : epsilon β Λ M ^ 2 / (κ * tau β Λ M) ≤ kappaPrimeEndpointExpratConstant β * epsilon β Λ (M - 1) ^ (2 * delta β)

The terminal ratio ε_M²/(κ τ_M) is controlled directly by the permitted interval and the M−1 time scale, with the one-sided exponent 2δ.

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

The uniform upper constant for the interior κ′ exprat estimate.

Equations

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

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

One constant covers the interior κ′ exprat estimate and the direct permitted-interval estimate at its terminal scale.

Equations

• AVenhance.Infra.Section3.kappaPrimeExpratGlobalUpperConstant β = max (AVenhance.Infra.Section3.kappaPrimeExpratUpperConstant β) (AVenhance.Infra.Section3.kappaPrimeEndpointExpratConstant β)

theorem AVenhance.Infra.Section3.kappaPrimeExpratUpperConstant_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < kappaPrimeExpratUpperConstant β

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaPrimeExpratGlobalUpperConstant_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < kappaPrimeExpratGlobalUpperConstant β

theorem AVenhance.Infra.Section3.kappaPrimeAt_exprat_global_upper {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) {m : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) : epsilon β Λ m ^ 2 / (kappaPrimeAt β Λ κ m (M - m) * tau β Λ m) ≤ kappaPrimeExpratGlobalUpperConstant β * epsilon β Λ (m - 1) ^ delta β

The κ′ exprat ratio, including the terminal scale, is bounded by one β-only constant times ε_{m−1}^δ.

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.coarse_recurrence_ratio_step {u v B D w R : ℝ} (hu : 0 < u) (hv : 0 < v) (hB : 0 < B) (hD : D = 40 / 9 * B) (hcurrent : max (u / v) (v / u) ≤ R) (hlo : u ≤ w) (hhi : w ≤ u + D / u) : max (w / (v + B / v)) ((v + B / v) / w) ≤ R * (1 + 40 / 9 * (B / v ^ 2))

The elementary coarse comparison for one enhancement step. It is used only when the finite-scale ratio is too large for the averaging estimate.

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

The scale error is dominated by a fixed geometric sequence.

noncomputable def AVenhance.Infra.Section3.kappaAtBootstrapTail (β E : ℝ) (n : ℕ) : ℝ

The geometric tail used to keep all high-scale recurrence comparisons inside the factor-two bootstrap.

Equations

• AVenhance.Infra.Section3.kappaAtBootstrapTail β E n = E * (128 ^ (-AVenhance.delta β)) ^ n / (1 - 128 ^ (-AVenhance.delta β))

theorem AVenhance.Infra.Section3.kappaAtBootstrapTail_succ {β E : ℝ} (n : ℕ) (hden : 1 - 128 ^ (-delta β) ≠ 0) : kappaAtBootstrapTail β E n = E * (128 ^ (-delta β)) ^ n + kappaAtBootstrapTail β E (n + 1)

One recurrence step splits off the first term of the geometric tail.

theorem AVenhance.Infra.Section3.exists_kappaAtBootstrap_cutoff {β E : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hE : 0 < E) : ∃ (N : ℕ), 1 ≤ N ∧ kappaAtBootstrapTail β E N ≤ 1 / 2

A finite cutoff can make the high-scale geometric tail as small as needed.

noncomputable def AVenhance.Infra.Section3.kappaAtBootstrapErrorCoefficient (β C₀ R : ℝ) : ℝ

The one-step error coefficient when the current actual/prime ratio is bounded by R.

Equations

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

noncomputable def AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapThreshold (β C₀ R : ℝ) : ℝ

A bad-step threshold determined by the current comparison bound.

Equations

• AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapThreshold β C₀ R = 1 / (2 * AVenhance.Infra.Section3.kappaAtBootstrapErrorCoefficient β C₀ R)

noncomputable def AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapBadEpsilonFloor (β C₀ R : ℝ) : ℝ

A lower bound for the next epsilon scale whenever a step is too coarse for the relative averaging estimate.

Equations

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

noncomputable def AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapBadIncrementCap (β C₀ R : ℝ) : ℝ

The prime increment ratio is uniformly bounded on a bad low-scale step.

Equations

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

noncomputable def AVenhance.Infra.Section3.kappaAtBootstrapStepFactor (β C₀ R : ℝ) : ℝ

The worst multiplicative loss of one low-scale step at ratio bound R.

Equations

• AVenhance.Infra.Section3.kappaAtBootstrapStepFactor β C₀ R = max 2 (1 + 40 / 9 * AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapBadIncrementCap β C₀ R)

def AVenhance.Infra.Section3.kappaAtBootstrapIteratedBound (β C₀ : ℝ) : ℕ → ℝ

Finite iteration of the coarse low-scale step factors.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section3.kappaAtBootstrapIteratedBound β C₀ 0 = 2

theorem AVenhance.Infra.Section3.kappaAtBootstrapErrorCoefficient_pos {β C₀ R : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hC₀ : 0 ≤ C₀) (hR : 1 ≤ R) : 0 < kappaAtBootstrapErrorCoefficient β C₀ R

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapThreshold_pos {β C₀ R : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hC₀ : 0 ≤ C₀) (hR : 1 ≤ R) : 0 < kappaAtBootstrapThreshold β C₀ R

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapErrorCoefficient_ge_one {β C₀ R : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hC₀ : 0 ≤ C₀) (hR : 1 ≤ R) : 1 ≤ kappaAtBootstrapErrorCoefficient β C₀ R

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaAtBootstrapStepFactor_ge_two {β C₀ R : ℝ} : 2 ≤ kappaAtBootstrapStepFactor β C₀ R

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.epsilon_le_one_over_128_local {β : ℝ} {Λ n : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hn : 1 ≤ n) : epsilon β Λ n ≤ 1 / 128

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.epsilon_next_lower_of_bad_threshold {β : ℝ} {Λ j : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hj : 2 ≤ j) {t : ℝ} (ht : 0 < t) (hbad : t < epsilon β Λ (j - 1) ^ delta β) : 1 / 2 * t ^ (q β / delta β) ≤ epsilon β Λ j

Every exceptional low-scale step has a β- and C₀-uniform lower bound on its next epsilon scale.

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaPrime_increment_ratio_internal_upper {β : ℝ} {Λ M j : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) (hj : 1 ≤ j) (hjM : j < M) : 9 / 80 * (a β Λ j ^ 2 * epsilon β Λ j ^ 4) / kappaPrimeAt β Λ κ j (M - j) ^ 2 ≤ 80 / 9 * kappaPrimeUniformConstant β ^ 2 * epsilon β Λ j ^ (-2 * gamma β)

On an interior scale, the normalized κ′ lower bound controls its relative enhancement increment.

theorem AVenhance.Infra.Section3.KappaAtPrimeBootstrap.kappaPrime_increment_ratio_terminal_upper {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) : 9 / 80 * (a β Λ M ^ 2 * epsilon β Λ M ^ 4) / κ ^ 2 ≤ 9 / 20

theorem AVenhance.Infra.Section3.kappaAtBootstrap_one_step {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {κ : ℝ} (hκ : 0 < κ) {M j : ℕ} (hpermitted : κ ∈ permittedInterval β I.Λ M) (hj : 2 ≤ j) (hjM : j ≤ M) {R : ℝ} (hR : 1 ≤ R) (hcurrent : max (I.kappaAt κ j (M - j) / kappaPrimeAt β I.Λ κ j (M - j)) (kappaPrimeAt β I.Λ κ j (M - j) / I.kappaAt κ j (M - j)) ≤ R) : max (I.KhomScalar (I.kappaAt κ j (M - j)) j / (kappaPrimeAt β I.Λ κ j (M - j) + 9 / 80 * (a β I.Λ j ^ 2 * epsilon β I.Λ j ^ 4) / kappaPrimeAt β I.Λ κ j (M - j))) ((kappaPrimeAt β I.Λ κ j (M - j) + 9 / 80 * (a β I.Λ j ^ 2 * epsilon β I.Λ j ^ 4) / kappaPrimeAt β I.Λ κ j (M - j)) / I.KhomScalar (I.kappaAt κ j (M - j)) j) ≤ R * kappaAtBootstrapStepFactor β C₀ R

A comparison step is controlled either by the averaging estimate with a small relative error or by the crude two-sided flux bound.

theorem AVenhance.Infra.Section3.kappaAtBootstrap_averaged_step {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {κ : ℝ} (hκ : 0 < κ) {M j : ℕ} (hpermitted : κ ∈ permittedInterval β I.Λ M) (hj : 2 ≤ j) (hjM : j ≤ M) {R : ℝ} (hR : 1 ≤ R) (hcurrent : max (I.kappaAt κ j (M - j) / kappaPrimeAt β I.Λ κ j (M - j)) (kappaPrimeAt β I.Λ κ j (M - j) / I.kappaAt κ j (M - j)) ≤ R) (hηsmall : kappaAtBootstrapErrorCoefficient β C₀ R * epsilon β I.Λ (j - 1) ^ delta β < 1) : have η := kappaAtBootstrapErrorCoefficient β C₀ R * epsilon β I.Λ (j - 1) ^ delta β; max (I.KhomScalar (I.kappaAt κ j (M - j)) j / (kappaPrimeAt β I.Λ κ j (M - j) + 9 / 80 * (a β I.Λ j ^ 2 * epsilon β I.Λ j ^ 4) / kappaPrimeAt β I.Λ κ j (M - j))) ((kappaPrimeAt β I.Λ κ j (M - j) + 9 / 80 * (a β I.Λ j ^ 2 * epsilon β I.Λ j ^ 4) / kappaPrimeAt β I.Λ κ j (M - j)) / I.KhomScalar (I.kappaAt κ j (M - j)) j) ≤ R / (1 - η)

Good-step comparison with the actual, summable relative error retained.

theorem AVenhance.Infra.Section3.kappaAtBootstrap_errorCoefficient_mono {β C₀ R S : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hC₀ : 0 ≤ C₀) (hRS : R ≤ S) : kappaAtBootstrapErrorCoefficient β C₀ R ≤ kappaAtBootstrapErrorCoefficient β C₀ S

theorem AVenhance.Infra.Section3.kappaAtBootstrapTail_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {E : ℝ} (hE : 0 ≤ E) (n : ℕ) : 0 ≤ kappaAtBootstrapTail β E n

theorem AVenhance.Infra.Section3.kappaAtBootstrapTail_le_half_of_index {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {E : ℝ} (hE : 0 < E) {N n : ℕ} (hN : kappaAtBootstrapTail β E N ≤ 1 / 2) (hn : N ≤ n) : kappaAtBootstrapTail β E n ≤ 1 / 2

theorem AVenhance.Infra.Section3.kappaAtBootstrapTail_step_bound {β η : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {E : ℝ} (hE : 0 < E) {m : ℕ} (hmTail : kappaAtBootstrapTail β E m ≤ 1 / 2) (hη0 : 0 ≤ η) (hη : η ≤ E * (128 ^ (-delta β)) ^ m) : (1 - kappaAtBootstrapTail β E (m + 1))⁻¹ / (1 - η) ≤ (1 - kappaAtBootstrapTail β E m)⁻¹

theorem AVenhance.Infra.Section3.kappaAtBootstrapIteratedBound_ge_two {β C₀ : ℝ} (n : ℕ) : 2 ≤ kappaAtBootstrapIteratedBound β C₀ n

theorem AVenhance.Infra.Section3.kappaAtBootstrapIteratedBound_pos {β C₀ : ℝ} (n : ℕ) : 0 < kappaAtBootstrapIteratedBound β C₀ n

theorem AVenhance.Infra.Section3.kappaAtBootstrapIteratedBound_mono {β C₀ : ℝ} {k n : ℕ} (hk : k ≤ n) : kappaAtBootstrapIteratedBound β C₀ k ≤ kappaAtBootstrapIteratedBound β C₀ n