Carleson/ToMathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem not_integrableOn_Ioi_rpow' line 11 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Neg.neg, Not, MeasureTheory.IntegrableOn, HPow.hPow, Set.Ioi, MeasureTheory.MeasureSpace.volume

    Proof uses: dite, Eq, Eq.mpr, id, congrArg, not_integrableOn_Ioi_rpow, LT.lt, propext, integrableOn_Ioi_rpow_iff, LE.le.lt_of_ne'

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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