OAI/Geometry/Convex/GeneralMahler/LayerMeasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

§02 scalar measure from the derivative of avH. Real densities here.

  1. lemma OAI.GeneralMahler.weighted_primitive_moments_pos line 11

    Source comment

    A scalar general lemma about finite moments from fast primitive decay.
    lemma weighted_primitive_moments_pos (f g F : ℝ → ℝ)
    (h : ∀ x, HasDerivAt f (g x) x) (hn : ∀ x, 0 ≤ g x)
    (c : ℝ) (hv : rapid F) (hmeas : Measurable F)
    (hf : ∀ x : ℝ, 0 < x → f x-c = F x) (n : ℕ) :
    IntegrableOn (fun x => g x*(1+x)^n) (Ioi 0) := by
…

    Mentions: OAI.GeneralMahler.rapid

  2. def OAI.GeneralMahler.ProjField.layerW line 51
  3. lemma OAI.GeneralMahler.ProjField.H_deriv line 53
  4. lemma OAI.GeneralMahler.ProjField.H_cont line 55
  5. lemma OAI.GeneralMahler.ProjField.w_cont line 58
  6. lemma OAI.GeneralMahler.ProjField.w_positive line 60
  7. lemma OAI.GeneralMahler.ProjField.H_infty line 63
  8. lemma OAI.GeneralMahler.ProjField.H_bot line 71
  9. theorem OAI.GeneralMahler.ProjField.w_moment line 83
  10. theorem OAI.GeneralMahler.ProjField.integrable_w line 116
  11. theorem OAI.GeneralMahler.ProjField.integral_w line 117