Golfing an integral

Stream: general

[Moritz Doll]

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],
    rw ←interval_integrable_iff_integrable_Ioc_of_le (le_add_of_nonneg_left hb),
    refine interval_integrable_rpow _,
    right,
    exact zero_nonmem b hb,
  end,
  have htendsto : tendsto (λ (b : ℝ≥0), (b : ℝ) + 1) at_top at_top :=
  begin
    apply tendsto_at_top_add_const_right,
    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],
    rw integrate_abs_of_nonneg (le_add_of_nonneg_left hb),
    { 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,
        exact tendsto_at_top_of_add_const_right 1 htendsto',
      end,
      exact tendsto.comp tendsto_nnreal htendsto', },
  end,
  exact integrable_on_Ioi_of_interval_integral_norm_tendsto _ _ finite_integrable htendsto hlimit,
end

[Bhavik Mehta]

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]

Wellintegrable_on_rpow_Ioi is what I want

[Moritz Doll]

could you PR that?

[Bhavik Mehta]

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

[Yaël Dillies]

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