QuadraticGrowthMatrixCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common matrix budget for each actual divisor band

theorem OAI.Ostmann.root_product_factor line 10

theorem OAI.Ostmann.quadratic_growth_band_root_bound line 29

Source documentation

The divisor-product upper cutoff gives one budget independent of the chosen two divisor blocks. The lower cutoff controls the geometry.

theorem quadratic_growth_band_root_bound {F Y N u v D E₁ E₂ : ℝ}
    (hF : 0 ≤ F) (hY : 0 ≤ Y) (hN : 0 ≤ N)
    (hu : 1 ≤ u) (hv : 1 ≤ v) (hD : 0 < D)
    (hP : u * v ≤ 2 * D) (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂) :
    Real.sqrt (2 * (F * (Y + N / u)) * u * E₁) *
      Real.sqrt (2 * (F * (Y + N / v)) * v * E₂) ≤
      8 * F * Real.sqrt D *
        (Y + Real.sqrt (Y * N) + N / Real.sqrt D) *
          (Real.sqrt E₁ * Real.sqrt E₂) := by
…