OAI/Analysis/Mahler/TailIntegral.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SymmetricMahler.inverse_sqrt_eq_rpow line 9
  2. lemma OAI.SymmetricMahler.inverse_sqrt_integrable line 13
  3. lemma OAI.SymmetricMahler.inverse_sqrt_integral line 22
  4. lemma OAI.SymmetricMahler.shifted_inverse_sqrt_integrable line 36
  5. lemma OAI.SymmetricMahler.shifted_inverse_sqrt_integral line 41
  6. theorem OAI.SymmetricMahler.tail_integrable line 47

    Source documentation

    The singular tail integral is well-defined even at its upper endpoint.

    theorem tail_integrable {L : ℝ} (hL : 0 < L) :
    IntervalIntegrable (fun t : ℝ => exp (-t) * sqrt (t/(L-t))) volume 0 L := by
…
  7. theorem OAI.SymmetricMahler.uniform_tail_integral line 66

    Source documentation

    The uniform-L integral estimate, including integrability at the singular endpoint.

    theorem uniform_tail_integral {L : ℝ} (hL : 0 < L) :
    (∫ t in (0 : ℝ)..L, exp (-t) * sqrt (t/(L-t))) ≤ 1 + 4/exp 1 := by
…
  8. lemma OAI.SymmetricMahler.rescaled_tail_ratio line 121
  9. theorem OAI.SymmetricMahler.rescaled_tail_integral line 128

    Source documentation

    The change of variables t=m(1-r) in the error tail, with normalization factors and endpoint orientations.

    theorem rescaled_tail_integral {m b : ℝ} (hm : 0 < m) :
    (∫ r in b..(1 : ℝ), m*exp (-m*(1-r))*sqrt ((1-r)/(r-b))) =
      ∫ t in (0 : ℝ)..m*(1-b), exp (-t)*sqrt (t/(m*(1-b)-t)) := by
…
  10. theorem OAI.SymmetricMahler.rescaled_tail_integrable line 146

    Source documentation

    Integrability also survives the affine rescaling in the error estimate.

    theorem rescaled_tail_integrable {m b : ℝ} (hm : 0 < m) (hb : b < 1) :
    IntervalIntegrable
      (fun r : ℝ => m*exp (-m*(1-r))*sqrt ((1-r)/(r-b))) volume b 1 := by
…
  11. theorem OAI.SymmetricMahler.rescaled_tail_bound line 161

    Source documentation

    The uniform bound after substitution, independent of b and m.

    theorem rescaled_tail_bound {m b : ℝ} (hm : 0 < m) (hb : b < 1) :
    (∫ r in b..(1 : ℝ), m*exp (-m*(1-r))*sqrt ((1-r)/(r-b))) ≤
      1 + 4/exp 1 := by
…
  12. lemma OAI.SymmetricMahler.right_inverse_sqrt_integrable line 172
  13. lemma OAI.SymmetricMahler.right_inverse_sqrt_integral line 177