pith. machine review for the scientific record. sign in
theorem proved tactic proof

ancientDecay_implies_A2_integrable

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  78theorem ancientDecay_implies_A2_integrable (P : RM2URadialProfile) (hD : AncientEnergyDecay P) :
  79    IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume := by

proof body

Tactic-mode proof.

  80  refine integrableOn_Ioi_of_rpow_decay (by norm_num : (-3 : ℝ) < -1) (sq_pos_of_pos hD.hC)
  81    (fun x hx => ((P.hA x hx).continuousAt.continuousWithinAt.pow 2)) ?_
  82  intro r hr
  83  have hr0 : 0 ≤ r := le_of_lt (lt_trans zero_lt_one (mem_Ioi.mp hr))
  84  rw [abs_of_nonneg (sq_nonneg (P.A r))]
  85  calc (P.A r) ^ 2 = |P.A r| ^ 2 := by rw [sq_abs]
  86    _ ≤ (hD.C * r ^ ((-3 : ℝ) / 2)) ^ 2 :=
  87        (sq_le_sq₀ (abs_nonneg _) (mul_nonneg hD.hC.le (Real.rpow_nonneg hr0 _))).2 (hD.decay r hr)
  88    _ = hD.C ^ 2 * r ^ (-3 : ℝ) := by
  89        rw [mul_pow, ← Real.rpow_natCast (r ^ ((-3 : ℝ) / 2)) 2, ← Real.rpow_mul hr0]; norm_num
  90
  91/-- `AncientEnergyDecay` implies `(A')² r² ∈ L¹(1,∞)` (the second half of `CoerciveL2Bound`).
  92    Decay: `|A'| ≤ C r^{-5/2}`, so `(A')²r² ≤ C² r^{-3}`, integrable since `-3 < -1`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.