Carleson/ToMathlib/Analysis/SpecialFunctions/Integrals/Basic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. theorem MeasureTheory.setLIntegral_Ioo_rpow line 14 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, ENNReal, LT.lt, Neg.neg, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioo, HPow.hPow, HDiv.hDiv, HSub.hSub, HAdd.hAdd, ENNReal.ofReal

    Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add and 133 more

    164 instances, coercions and auxiliary constants left out.

    Tactic trace: 64 steps

    Open to load the checked before-and-after goal states.

  2. theorem MeasureTheory.setLIntegral_Iio_rpow line 77 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, ENNReal, LT.lt, Neg.neg, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, HPow.hPow, HDiv.hDiv, HAdd.hAdd, ENNReal.ofReal

    Proof uses: Set.Ioo, HSub.hSub, MeasureTheory.setLIntegral_Ioo_rpow, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.setLIntegral_congr, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, Set.Ico, Bot.bot, id, congrArg, Set, Set.Ico_bot, Filter.EventuallyEq.symm and 47 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.