OAI/Analysis/HenonEmden/Tails.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HenonLaneEmden.UniformTail.dyadic_power_identity line 13
2. lemma OAI.HenonLaneEmden.UniformTail.lintegral_norm_rpow_compl_ball_le line 32

   Source documentation

   A nonnegative measure having polynomial centered ball growth has a uniform inverse-power tail whenever the decay exponent exceeds the growth exponent. The proof uses a geometric majorant, not subtraction of divergent potentials.

   lemma lintegral_norm_rpow_compl_ball_le (μ : Measure E) {C R a s : ℝ}
       (hC : 0 ≤ C) (hR : 0 < R) (ha : 0 ≤ a) (hs : s < a)
       (hball : ∀ r > 0, μ (Metric.ball (0:E) r) ≤ ENNReal.ofReal (C*r^s)) :
       (∫⁻ y in (Metric.ball (0:E) R)ᶜ, ENNReal.ofReal (‖y‖^(-a)) ∂μ) ≤
         ENNReal.ofReal (C*2^s*R^(s-a)/(1-2^(s-a))) := by
   …