Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324DerivativeLossAbsorption

Numerical absorption of fixed-cutoff derivative losses #

A fixed smooth cutoff may contribute an order-dependent loss of the form m⁸ Cderiv^m. This module records a deliberately coarse, purely numerical ledger which absorbs that loss by enlarging both named constants in the R-324 geometric amplitude. It assumes no routing certificate and no analytic estimate.

source
def Anderson4D.r324DerivativeAbsorptionBase (Cderiv : ℝ) :
ℝ

The fixed base used to absorb an eighth-degree order loss together with a cutoff-dependent geometric loss.

Equations
Instances For
    source
    theorem Anderson4D.one_le_r324DerivativeAbsorptionBase (Cderiv : ℝ) :
    1 ≤ r324DerivativeAbsorptionBase Cderiv

    The absorption base is at least one, with no sign assumption on the cutoff-dependent input.

    source
    theorem Anderson4D.r324_nat_pow_eight_le_256_pow (m : ℕ) (hm : 1 ≤ m) :
    m ^ 8 ≤ 256 ^ m

    Elementary natural-number growth ledger: m⁸ costs at most the fixed geometric base 256^m for m ≥ 1.

    source
    theorem Anderson4D.r324_real_natCast_pow_eight_le_256_pow (m : ℕ) (hm : 1 ≤ m) :
    ↑m ^ 8 ≤ 256 ^ m

    Real-cast form of r324_nat_pow_eight_le_256_pow.

    source
    theorem Anderson4D.r324_pow_le_self_mul_pow_double_sub_two {A : ℝ} {m : ℕ} (hA : 1 ≤ A) (hm : 1 ≤ m) :
    A ^ m ≤ A * A ^ (2 * m - 2)

    For a base at least one, the longer R-324 exponent 2m-2, together with one outer copy, absorbs a power with exponent m.

    source
    theorem Anderson4D.r324_derivative_order_loss_le_absorptionBase_mul_power {Cderiv : ℝ} {m : ℕ} (hCderiv : 0 ≤ Cderiv) (hm : 1 ≤ m) :
    ↑m ^ 8 * Cderiv ^ m ≤ r324DerivativeAbsorptionBase Cderiv * r324DerivativeAbsorptionBase Cderiv ^ (2 * m - 2)

    The raw fixed-cutoff loss is absorbed by one outer copy and the full 2m-2 geometric power of r324DerivativeAbsorptionBase Cderiv.

    source
    theorem Anderson4D.r324_derivative_order_loss_absorbed_by_outer_and_power {outerConstant powerConstant Cderiv lam : ℝ} {m : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCderiv : 0 ≤ Cderiv) (hlam : 0 ≤ lam) (hm : 1 ≤ m) :
    outerConstant * (↑m ^ 8 * Cderiv ^ m) * (powerConstant * lam) ^ (2 * m - 2) ≤ outerConstant * r324DerivativeAbsorptionBase Cderiv * (powerConstant * r324DerivativeAbsorptionBase Cderiv * lam) ^ (2 * m - 2)

    Independent outer/power absorption ledger.

    If a derivative estimate contributes m⁸ Cderiv^m in front of the usual geometric factor, it is enough to make the two independent replacements

    This is the scalar inequality needed by a later analytic routing theorem.