PFR/Mathlib/Probability/UniformOn.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 3 files
  1. lemma ProbabilityTheory.uniformOn_apply_singleton_of_mem line 14 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Membership.mem, Set.Finite, Eq, ENNReal, MeasureTheory.Measure, ProbabilityTheory.uniformOn, Singleton.singleton, HDiv.hDiv, OfNat.ofNat, Nat.card

    Proof uses: Inter.inter, Set.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, congrFun', Set.inter_eq_left', LE.le, eq_true, iff_self, Eq.mpr, MeasureTheory.Measure.count, id, Inv.inv, HSMul.hSMul, MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrict_apply and 10 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. lemma ProbabilityTheory.real_uniformOn_apply_singleton_of_mem line 21 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Membership.mem, Set.Finite, Eq, Real, MeasureTheory.Measure.real, ProbabilityTheory.uniformOn, Singleton.singleton, HDiv.hDiv, OfNat.ofNat, Nat.card

    Proof uses: of_eq_true, Eq.trans, Inv.inv, Set.ncard, True, congr, congrArg, ENNReal.toReal, MeasureTheory.Measure, ENNReal, ProbabilityTheory.uniformOn_apply_singleton_of_mem, one_div, ENNReal.toReal_inv, ENNReal.toReal_natCast, eq_self

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma ProbabilityTheory.uniformOn_apply_singleton_of_not_mem line 25 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Not, Membership.mem, Eq, ENNReal, MeasureTheory.Measure, ProbabilityTheory.uniformOn, Singleton.singleton, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, Inv.inv, MeasureTheory.Measure.count, MeasureTheory.Measure.restrict, Inter.inter, MeasureTheory.Measure.restrict_apply, MeasurableSet, EmptyCollection.emptyCollection, Set.singleton_inter_of_notMem, False, eq_false, not_false_eq_true, MeasureTheory.measure_empty, MulZeroClass.mul_zero, eq_self

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma ProbabilityTheory.real_uniformOn_apply_singleton_of_not_mem line 28 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Not, Membership.mem, Eq, Real, MeasureTheory.Measure.real, ProbabilityTheory.uniformOn, Singleton.singleton, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ENNReal, MeasureTheory.Measure, ENNReal.toReal, ProbabilityTheory.uniformOn_apply_singleton_of_not_mem, eq_self

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem ProbabilityTheory.uniformOn_apply_eq_zero line 32 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Eq, Inter.inter, EmptyCollection.emptyCollection, ENNReal, MeasureTheory.Measure, ProbabilityTheory.uniformOn, OfNat.ofNat

    Proof uses: Set.Finite, Set.Infinite, Or, Set.finite_or_infinite, Iff.mpr, ProbabilityTheory.uniformOn_eq_zero_iff, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, Inv.inv, MeasureTheory.Measure.count, MeasureTheory.Measure.restrict, Top.top, MeasureTheory.Measure.count_apply_infinite, ENNReal.inv_top, zero_smul, eq_self

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. lemma ProbabilityTheory.uniformOn_of_infinite line 37 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Set.Infinite, Eq, MeasureTheory.Measure, ProbabilityTheory.uniformOn, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, Or, EmptyCollection.emptyCollection, True, congrFun', congrArg, eq_true, true_or

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma ProbabilityTheory.uniformOn_apply line 39 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Set.Finite, Eq, ENNReal, MeasureTheory.Measure, ProbabilityTheory.uniformOn, HDiv.hDiv, Nat.card, Inter.inter

    Proof uses: Eq.mpr, ProbabilityTheory.cond, MeasureTheory.Measure.count, id, congrArg, ProbabilityTheory.uniformOn.eq_1, HMul.hMul, Inv.inv, ProbabilityTheory.cond_apply, Set.Finite.measurableSet, Finset.card, Set.Finite.toFinset, MeasureTheory.Measure.count_apply_finite, Set.Finite.inter_of_left, Nat, Eq.symm, Nat.card_eq_card_finite_toFinset, ENNReal.div_eq_inv_mul, Eq.refl

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma ProbabilityTheory.uniformOn_real line 45 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Set.Finite, Eq, Real, MeasureTheory.Measure.real, ProbabilityTheory.uniformOn, HDiv.hDiv, Nat.card, Inter.inter

    Proof uses: of_eq_true, Set.ncard, Eq.trans, True, congrFun', congrArg, ENNReal.toReal, MeasureTheory.Measure, ENNReal, ProbabilityTheory.uniformOn_apply, ENNReal.toReal_div, congr, ENNReal.toReal_natCast, eq_self

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. lemma ProbabilityTheory.uniformOn_real_singleton line 49 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Set.Finite, Decidable, Membership.mem, Eq, Real, MeasureTheory.Measure.real, ProbabilityTheory.uniformOn, Singleton.singleton, ite, Inv.inv, Set.ncard, OfNat.ofNat

    Proof uses: Eq.mpr, HDiv.hDiv, id, congrFun', congrArg, Eq.trans, Nat.card, Inter.inter, ProbabilityTheory.uniformOn_real, Nat, Set.ncard_inter_singleton, Nat.cast_ite, ite_congr, Eq.refl, Nat.cast_one, Not, CharP.cast_eq_zero, dite, congr, ite_eq_left and 6 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  10. instance ProbabilityTheory.uniformOn.instIsProbabilityMeasure line 53 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Nonempty, Finite, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.uniformOn

    Proof uses: ProbabilityTheory.isProbabilityMeasure_uniformOn, Set.Nonempty.of_subtype

    2 instances, coercions and auxiliary constants left out.

  11. lemma ProbabilityTheory.map_uniformOn_apply line 56 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Measurable, Function.Injective, MeasurableSet, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.Measure.map, ProbabilityTheory.uniformOn, Set.image

    Proof uses: Set.Infinite, Set.Finite, Or, Set.infinite_or_finite, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, congrFun', ProbabilityTheory.uniformOn_of_infinite, MeasureTheory.Measure.map_zero, Set.Infinite.image, Function.Injective.injOn, eq_self, Eq.mpr, Set.preimage, id, MeasureTheory.Measure.map_apply and 10 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  12. lemma ProbabilityTheory.map_uniformOn line 64 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Measurable, Function.Injective, Eq, MeasureTheory.Measure, MeasureTheory.Measure.map, ProbabilityTheory.uniformOn, Set.image

    Proof uses: MeasureTheory.Measure.ext, MeasurableSet, ProbabilityTheory.map_uniformOn_apply

    Tactic trace: 2 steps

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