Documentation Verification Report

Cauchy

📁 Source: Mathlib/Probability/Distributions/Cauchy.lean

Statistics

Metric	Count
Definitions `cauchyMeasure`, `cauchyPDF`, `cauchyPDFReal`	3
Theorems `cauchyMeasure_of_scale_ne_zero`, `cauchyMeasure_zero_scale`, `cauchyPDFReal_def`, `cauchyPDFReal_def'`, `cauchyPDFReal_scale_zero`, `cauchyPDF_def`, `cauchyPDF_pos`, `cauchyPDF_scale_zero`, `instIsProbabilityMeasure_cauchyMeasure`, `integrable_cauchyPDFReal`, `integral_cauchyPDFReal`, `lintegral_cauchyPDF_eq_one`, `measurable_cauchyPDF`, `measurable_cauchyPDFReal`, `stronglyMeasurable_cauchyPDF`, `stronglyMeasurable_cauchyPDFReal`	16
Total	19

Probability

Definitions

Name	Category	Theorems
`cauchyMeasure` 📖	CompOp	3 math math: `cauchyMeasure_of_scale_ne_zero`, `cauchyMeasure_zero_scale`, `instIsProbabilityMeasure_cauchyMeasure`
`cauchyPDF` 📖	CompOp	6 math math: `cauchyMeasure_of_scale_ne_zero`, `cauchyPDF_scale_zero`, `stronglyMeasurable_cauchyPDF`, `lintegral_cauchyPDF_eq_one`, `cauchyPDF_def`, `measurable_cauchyPDF`
`cauchyPDFReal` 📖	CompOp	9 math math: `measurable_cauchyPDFReal`, `integral_cauchyPDFReal`, `cauchyPDF_pos`, `cauchyPDFReal_scale_zero`, `cauchyPDFReal_def'`, `cauchyPDF_def`, `stronglyMeasurable_cauchyPDFReal`, `integrable_cauchyPDFReal`, `cauchyPDFReal_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchyMeasure_of_scale_ne_zero` 📖	mathematical	—	`cauchyMeasure` `MeasureTheory.Measure.withDensity` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `cauchyPDF`	—	—
`cauchyMeasure_zero_scale` 📖	mathematical	—	`cauchyMeasure` `NNReal` `instZeroNNReal` `MeasureTheory.Measure.dirac` `Real` `Real.measurableSpace`	—	—
`cauchyPDFReal_def` 📖	mathematical	—	`cauchyPDFReal` `Real` `Real.instMul` `Real.instInv` `Real.pi` `NNReal.toReal` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub`	—	—
`cauchyPDFReal_def'` 📖	mathematical	—	`cauchyPDFReal` `Real` `Real.instMul` `Real.instInv` `Real.pi` `NNReal.toReal` `NNReal` `NNReal.instInv` `Real.instAdd` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub`	—	`cauchyPDFReal_def` `MulZeroClass.mul_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero` `MulZeroClass.zero_mul` `inv_zero` `div_zero` `inv_one` `mul_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Real.pi_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add`
`cauchyPDFReal_scale_zero` 📖	mathematical	—	`cauchyPDFReal` `NNReal` `instZeroNNReal` `Pi.instZero` `Real` `Real.instZero`	—	`MulZeroClass.mul_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero` `MulZeroClass.zero_mul`
`cauchyPDF_def` 📖	mathematical	—	`cauchyPDF` `ENNReal.ofReal` `cauchyPDFReal`	—	—
`cauchyPDF_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `cauchyPDFReal`	—	`cauchyPDFReal_def` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.pi_pos` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass`
`cauchyPDF_scale_zero` 📖	mathematical	—	`cauchyPDF` `NNReal` `instZeroNNReal` `Pi.instZero` `Real` `ENNReal` `instZeroENNReal`	—	`cauchyPDFReal_scale_zero` `ENNReal.ofReal_zero`
`instIsProbabilityMeasure_cauchyMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Real` `Real.measurableSpace` `cauchyMeasure`	—	`cauchyMeasure_zero_scale` `MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `cauchyMeasure_of_scale_ne_zero` `MeasureTheory.withDensity_apply` `MeasureTheory.Measure.restrict_univ` `lintegral_cauchyPDF_eq_one`
`integrable_cauchyPDFReal` 📖	mathematical	—	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `cauchyPDFReal` `MeasureTheory.MeasureSpace.volume`	—	`cauchyPDFReal_scale_zero` `MeasureTheory.integrable_zero` `MeasureTheory.Integrable.of_integral_ne_zero` `integral_cauchyPDFReal` `NeZero.charZero_one` `RCLike.charZero_rclike`
`integral_cauchyPDFReal` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `cauchyPDFReal` `Real.instOne`	—	`cauchyPDFReal_def'` `MeasureTheory.integral_const_mul` `MeasureTheory.integral_sub_right_eq_self` `ContinuousAdd.measurableAdd` `Real.borelSpace` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `MeasureTheory.Measure.integral_comp_div` `NNReal.abs_eq` `integral_univ_inv_one_add_sq` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Real.pi_pos` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one`
`lintegral_cauchyPDF_eq_one` 📖	mathematical	—	`MeasureTheory.lintegral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `cauchyPDF` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.toReal_eq_one_iff` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `LT.lt.le` `cauchyPDF_pos` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `stronglyMeasurable_cauchyPDFReal` `integral_cauchyPDFReal`
`measurable_cauchyPDF` 📖	mathematical	—	`Measurable` `Real` `ENNReal` `Real.measurableSpace` `ENNReal.measurableSpace` `cauchyPDF`	—	`Measurable.ennreal_ofReal` `measurable_cauchyPDFReal`
`measurable_cauchyPDFReal` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `cauchyPDFReal`	—	`Measurable.const_mul` `ContinuousMul.measurableMul` `Real.borelSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measurable.inv` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Measurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `Measurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `instSecondCountableTopologyReal` `Measurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `measurable_id'`
`stronglyMeasurable_cauchyPDF` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `ENNReal` `ENNReal.instTopologicalSpace` `Real.measurableSpace` `cauchyPDF`	—	`Measurable.stronglyMeasurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `ENNReal.instSecondCountableTopology` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `measurable_cauchyPDF`
`stronglyMeasurable_cauchyPDFReal` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.measurableSpace` `cauchyPDFReal`	—	`Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `measurable_cauchyPDFReal`

---

← Back to Index