Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 3 files
  1. lemma MemLp.toLp_sum line 11 source

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

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NormedAddCommGroup, Finset, Membership.mem, MeasureTheory.MemLp, Eq, Subtype, MeasureTheory.AEEqFun, AddSubgroup, MeasureTheory.Lp, MeasureTheory.MemLp.toLp, Finset.sum, MeasureTheory.memLp_finsetSum', Finset.univ, Finset.coe_mem

    Proof uses: MeasureTheory.Lp.ext, Eq.mpr, Filter.EventuallyEq, MeasureTheory.ae, id, congrArg, Subtype.val.eq_1, AddSubgroup.val_finsetSum, Iff.mp, MeasureTheory.AEEqFun.ext_iff, AEEqFun.mk_sum, MeasureTheory.MemLp.aestronglyMeasurable

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. theorem MeasureTheory.one_le_LpAddConst line 23 source

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

    Statement uses: ENNReal, LE.le, OfNat.ofNat, ENNReal.LpAddConst

    Proof uses: id, dite, ite, Membership.mem, Set, Set.Ioo, HPow.hPow, Real, HSub.hSub, HDiv.hDiv, ENNReal.toReal, Eq.mpr, Eq, congrArg, ite_eq_left, ENNReal.one_le_rpow, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl and 24 more

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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