Carleson/Classical/VanDerCorput.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma ContinuousOn.intervalIntegrable_Ioo_of_bound line 14 source

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

    Statement uses: Real, Complex, ContinuousOn, Set.Ioo, LE.le, Membership.mem, Set, Norm.norm, IntervalIntegrable, MeasureTheory.MeasureSpace.volume

    Proof uses: Eq.mpr, MeasureTheory.IntegrableOn, id, Eq, congrArg, propext, intervalIntegrable_iff_integrableOn_Ioo_of_le, enorm_ne_top, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.Measure.restrict, MeasureTheory.HasFiniteIntegral, ContinuousOn.aestronglyMeasurable, measurableSet_Ioo, MeasureTheory.HasFiniteIntegral.restrict_of_bounded, of_eq_true, LT.lt, ENNReal, MeasureTheory.Measure, Top.top and 11 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. lemma intervalIntegrable_continuous_mul_lipschitzOnWith line 23 source

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

    Statement uses: Real, NNReal, Complex, LE.le, Continuous, LipschitzOnWith, Set.Ioo, IntervalIntegrable, HMul.hMul, MeasureTheory.MeasureSpace.volume

    Proof uses: Eq, LT.lt, Or, LE.le.eq_or_lt, of_eq_true, Membership.mem, Set, Set.image, Set.Icc, Norm.norm, Exists, Bornology.IsBounded.exists_norm_le, IsCompact.isBounded, IsCompact.image_of_continuousOn, CompactIccSpace.isCompact_Icc, Continuous.continuousOn, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Nat and 106 more

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  3. lemma van_der_Corput line 53 source

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

    Statement uses: Real, LE.le, Int, Complex, NNReal, LipschitzOnWith, Set.Ioo, Membership.mem, Set, Norm.norm, intervalIntegral, HMul.hMul, Complex.exp, Complex.I, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Nat, Real.pi, HSub.hSub, HAdd.hAdd and 3 more

    Proof uses: mul_nonneg, of_eq_true, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq and 250 more

    377 instances, coercions and auxiliary constants left out.

    Tactic trace: 232 steps (first 200 of 232)

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