English
If p ∈ (0,1), then −1/(2(p−1)) ≤ ∫_{0}^{∞} rpowIntegrand₀₁(p,t,1) dt.
Русский
Пусть p ∈ (0,1); тогда −1/(2(p−1)) ≤ ∫_{0}^{∞} rpowIntegrand₀₁(p,t,1) dt.
LaTeX
$$$p \in (0,1)\Rightarrow -\frac{1}{2(p-1)} \le \int_{0}^{\infty} rpowIntegrand_{01}(p,t,1)\, dt$$$
Lean4
theorem le_integral_rpowIntegrand₀₁_one (hp : p ∈ Ioo 0 1) : -1 / (2 * (p - 1)) ≤ ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 :=
calc
_ = (1 / 2) * -((1 : ℝ) ^ (p - 1)) / (p - 1) := by rw [← div_div]; simp [neg_div]
_ = ∫ t in Ioi 1, (1 / 2) * t ^ (p - 2) := by
simp only [mem_Ioo] at hp
rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith) zero_lt_one]
ring_nf -- ring alone succeeds but gives a warning
_ ≤ ∫ t in Ioi 1, rpowIntegrand₀₁ p t 1 :=
by
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_
· refine Integrable.const_mul ?_ _
simp only [mem_Ioo] at hp
exact integrableOn_Ioi_rpow_of_lt (by linarith) zero_lt_one
· exact integrableOn_rpowIntegrand₀₁_Ioi_one hp zero_le_one
· exact fun t ht => rpowIntegrand₀₁_one_ge_rpow_sub_two hp (le_of_lt ht)
_ ≤ ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 :=
by
refine setIntegral_mono_set (integrableOn_rpowIntegrand₀₁_Ioi hp zero_le_one) ?_ ?_
· refine ae_restrict_of_forall_mem measurableSet_Ioi fun t ht => ?_
exact rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht) zero_le_one
· exact .of_forall <| Set.Ioi_subset_Ioi zero_le_one
