## Stream: general

### Topic: Golfing an integral

#### Moritz Doll (Sep 05 2022 at 22:55):

Hi, I have this very bad code for showing that the function x^y is integrable for fixed y < -1. I have trouble with coercion things and I suspect that my approach is not the right one and I should do something fundamentally different. Also I feel like the calculation of the integral should be an easy consequence of the stuff that I am doing, but it gets really annoying with more coercion and removing the absolute values. Any hint on what I am doing wrong would be appreciated.

import measure_theory.integral.integral_eq_improper
import analysis.special_functions.integrals

open measure_theory filter interval_integral
open_locale nnreal topological_space

lemma integrate_abs_of_nonneg {a b : ℝ} (hab : a ≤ b) {f : ℝ → ℝ} (hf : ∀ y (ha : y ∈ set.Icc a b), 0 ≤ f y) :
∫ (x : ℝ) in a .. b, |f x| ∂volume = ∫ (x : ℝ) in a .. b, f x ∂volume :=
begin
refine integral_congr _,
rintros x ⟨hx1, hx2⟩,
simp only [hab, max_eq_right, min_eq_left] at hx1 hx2,
simp [hf x ⟨hx1, hx2⟩],
end

lemma integrate_rpow_Ioi {y : ℝ} (hy : y < -1) : integrable_on (λ x, x^y) (set.Ioi (1 : ℝ)) volume :=
begin
have zero_nonmem : ∀ (b : ℝ) (hb : 0 ≤ b), (0 : ℝ) ∉ set.interval 1 (b + 1) :=
begin
intros b hb,
refine not_and_distrib.mpr _,
simp only [min_le_iff, le_max_iff, zero_le_one, true_or, not_true, or_false],
refine not_or_distrib.mpr _,
simp only [not_le, zero_lt_one, true_and],
positivity,
end,
have hy' : y + 1 ≠ 0 := ne_of_lt (lt_neg_iff_add_neg.mp hy),

have finite_integrable : ∀ (b : ℝ≥0), integrable_on (λ x, x^y) (set.Ioc (1 : ℝ) ((b+1) : ℝ)) volume :=
begin
rintro ⟨b, hb⟩,
simp only [subtype.coe_mk],
refine interval_integrable_rpow _,
right,
exact zero_nonmem b hb,
end,
have htendsto : tendsto (λ (b : ℝ≥0), (b : ℝ) + 1) at_top at_top :=
begin
simp only [nnreal.tendsto_coe_at_top],
exact tendsto_id,
end,
have htendsto' : tendsto (λ x : ℝ≥0, x + 1) at_top at_top :=
begin
simp_rw [←nnreal.coe_one, ←nnreal.coe_add, nnreal.tendsto_coe_at_top] at htendsto,
exact htendsto,
end,
have finite_integral : ∀ (b : ℝ≥0), ∫ (x : ℝ) in (1 : ℝ)..(b+1), |x^y| ∂volume =
( (b + 1 : ℝ) ^ (y + 1) - (1 : ℝ) ^ (y + 1)) / (y + 1) :=
begin
rintro ⟨b, hb⟩,
simp only [subtype.coe_mk],
{ exact integral_rpow (or.inr ⟨ne_of_lt hy, zero_nonmem b hb⟩) },
intros r hr,
exact real.rpow_nonneg_of_nonneg (zero_le_one.trans hr.1) _,
end,
let limit : ℝ := ((0 - 1) / (y + 1)),
have hlimit : tendsto (λ (b : ℝ≥0), ∫ (x : ℝ) in (1 : ℝ)..(b+1), ∥x^y∥ ∂volume) at_top (𝓝 limit) :=
begin
simp only [real.norm_eq_abs],
simp_rw finite_integral,
simp only [real.one_rpow],
refine tendsto.div _ tendsto_const_nhds hy',
{ refine tendsto.sub_const _ _,
have tendsto_real : tendsto (λ (b : ℝ), (b : ℝ) ^ (y + 1)) at_top (𝓝 (0)) :=
begin
rw ←neg_neg (y + 1),
refine tendsto_rpow_neg_at_top _,
simp [hy],
end,
have tendsto_nnreal: tendsto (λ (b : ℝ≥0), (b : ℝ) ^ (y + 1)) at_top (𝓝 (0)) :=
begin
refine tendsto.comp tendsto_real _,
norm_cast,
end,
exact tendsto.comp tendsto_nnreal htendsto', },
end,
exact integrable_on_Ioi_of_interval_integral_norm_tendsto _ _ finite_integrable htendsto hlimit,
end


#### Bhavik Mehta (Sep 05 2022 at 23:00):

I have some results in this direction which might be useful to you here, as part of the unit fractions project: https://github.com/b-mehta/unit-fractions/blob/master/src/for_mathlib/integral_rpow.lean

#### Moritz Doll (Sep 05 2022 at 23:03):

Wellintegrable_on_rpow_Ioi is what I want

#### Moritz Doll (Sep 05 2022 at 23:05):

could you PR that?

#### Bhavik Mehta (Sep 06 2022 at 00:49):

I will try to, but you may also feel free, I may not have time unfortunately

#### Yaël Dillies (Sep 06 2022 at 06:55):

Doesn't that follow from convexity? I was PRing convexity from LTE.

Last updated: Aug 03 2023 at 10:10 UTC