OAI/NumberTheory/Ostmann/Quadratic/QuadraticGrowthBandBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The common band budget has the required low/high recursive size

  1. def OAI.Ostmann.quadraticGrowthBandBudget line 9
  2. theorem OAI.Ostmann.quadratic_growth_band_budget_nonneg line 12
  3. theorem OAI.Ostmann.quadratic_first_growth_band_balance line 20

    Source documentation

    The minimum comes from the two outer corrections, with the actual normalizations M/N and sqrt(M)/(sqrt(B)D).

    theorem quadratic_first_growth_band_balance {M N B D F Y E : ℝ}
    (hM : 0 < M) (hN : 0 < N) (hB : 0 < B) (hD : 1 ≤ D)
    (hF : 0 ≤ F) (hY : 0 ≤ Y) (hE : 0 ≤ E) :
    min (M / N) (Real.sqrt M / (Real.sqrt B * D)) *
        quadraticGrowthBandBudget F Y N D E ≤
      16 * F * (M + Real.sqrt M / Real.sqrt B * Y) * E := by
…

    Mentions: OAI.Ostmann.quadraticGrowthBandBudget

  4. theorem OAI.Ostmann.quadratic_second_growth_band_balance line 46