AutoSamplingTheory.TechnicalLemmas.Algebra.ReciprocalGrowthRate

- Reciprocal growth converts to the usual `A / t` upper bound.

theorem reciprocal_growth_implies_inverse_time_bound
    {k k0 A t : ℝ}
    (hk : 0 < k) (hk0 : 0 < k0) (hA : 0 < A) (ht : 0 < t)
    (hgrowth : 1 / k0 + t / A ≤ 1 / k) :
    k ≤ A / t := by
  have hk0inv : 0 ≤ 1 / k0 := one_div_nonneg.mpr (le_of_lt hk0)
  have hbase : t / A ≤ 1 / k := by
    linarith
  have hta : t ≤ A / k := by
    have h := (div_le_iff₀ hA).mp hbase
    simpa [div_eq_mul_inv, mul_comm] using h
  have htk : t * k ≤ A := (le_div_iff₀ hk).mp hta
  have hkt : k * t ≤ A := by
    simpa [mul_comm] using htk
  exact (le_div_iff₀ ht).2 hkt

end Algebra
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Algebra/ReciprocalGrowthRate.lean:16published source at 7bcd37294df1