theorem
proved
tactic proof
bet1_boundaryTerm_integrable_of_L2_mul_r
show as:
view Lean formalization →
formal statement (Lean)
76theorem bet1_boundaryTerm_integrable_of_L2_mul_r
77 (P : RM2URadialProfile)
78 (hA2r : IntegrableOn (fun r : ℝ => (P.A r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume)
79 (hA'2r : IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume) :
80 IntegrableOn (fun r : ℝ => (-P.A r) * ((P.A' r) * (r ^ 2))) (Set.Ioi (1 : ℝ)) volume := by
proof body
Tactic-mode proof.
81 classical
82 -- Work on the restricted measure.
83 let μ := (volume.restrict (Set.Ioi (1 : ℝ)))
84
85 -- Show `(-A r)*r ∈ L²` and `(A' r)*r ∈ L²`.
86 have hcontA : ContinuousOn P.A (Set.Ioi (1 : ℝ)) := by
87 intro x hx
88 exact (P.hA x hx).continuousAt.continuousWithinAt
89 have hcontA' : ContinuousOn P.A' (Set.Ioi (1 : ℝ)) := by
90 intro x hx
91 exact (P.hA' x hx).continuousAt.continuousWithinAt
92 have hf_meas : AEStronglyMeasurable (fun r : ℝ => (-P.A r) * r) μ := by
93 have hcont : ContinuousOn (fun r : ℝ => (-P.A r) * r) (Set.Ioi (1 : ℝ)) := by
94 simpa using (hcontA.neg.mul (continuous_id.continuousOn))
95 exact hcont.aestronglyMeasurable measurableSet_Ioi
96 have hg_meas : AEStronglyMeasurable (fun r : ℝ => (P.A' r) * r) μ := by
97 have hcont : ContinuousOn (fun r : ℝ => (P.A' r) * r) (Set.Ioi (1 : ℝ)) := by
98 simpa using (hcontA'.mul (continuous_id.continuousOn))
99 exact hcont.aestronglyMeasurable measurableSet_Ioi
100
101 have hf_L2 : MeasureTheory.MemLp (fun r : ℝ => (-P.A r) * r) 2 μ := by
102 -- use `memLp_two_iff_integrable_sq`
103 refine (MeasureTheory.memLp_two_iff_integrable_sq (μ := μ) hf_meas).2 ?_
104 -- square equals `A^2 * r^2`
105 have : Integrable (fun r : ℝ => (P.A r) ^ 2 * (r ^ 2)) μ := by
106 simpa [MeasureTheory.IntegrableOn, μ] using hA2r
107 -- rewrite the integrand
108 simpa [pow_two, μ, mul_assoc, mul_left_comm, mul_comm] using this
109
110 have hg_L2 : MeasureTheory.MemLp (fun r : ℝ => (P.A' r) * r) 2 μ := by
111 refine (MeasureTheory.memLp_two_iff_integrable_sq (μ := μ) hg_meas).2 ?_
112 have : Integrable (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) μ := by
113 simpa [MeasureTheory.IntegrableOn, μ] using hA'2r
114 simpa [pow_two, μ, mul_assoc, mul_left_comm, mul_comm] using this
115
116 -- L² × L² → L¹ by Hölder (p=q=2, r=1).
117 have hprod : Integrable (fun r : ℝ => ((-P.A r) * r) * ((P.A' r) * r)) μ := by
118 -- `HolderTriple 2 2 1` is an instance
119 simpa [Pi.mul_def] using (MeasureTheory.MemLp.integrable_mul (μ := μ) hf_L2 hg_L2)
120
121 -- rewrite the product as the boundary term.
122 have : Integrable (fun r : ℝ => (-P.A r) * ((P.A' r) * (r ^ 2))) μ := by
123 -- pointwise: `((-A)*r) * ((A')*r) = (-A) * (A' * r^2)`
124 refine hprod.congr ?_
125 refine (ae_restrict_mem measurableSet_Ioi).mono ?_
126 intro r hr
127 ring
128 simpa [MeasureTheory.IntegrableOn, μ] using this
129
130/-- Convenience wrapper: if `CoerciveL2Bound P` holds, it suffices to prove only the stronger
131weighted \(L^2\) tail moment `∫ (A^2 * r^2) < ∞` to get `B ∈ L¹`. -/