Documentation Verification Report

Measure

📁 Source: Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean

Statistics

Metric	Count
Definitions `Measure`	1
Theorems `disjoint_residual_ae`, `ae_not_liouville`, `ae_not_liouvilleWith`, `setOf_liouvilleWith_subset_aux`, `volume_iUnion_setOf_liouvilleWith`, `volume_setOf_liouville`	6
Total	7

MeasCat

Definitions

Name	Category	Theorems
`Measure` 📖	CompOp	—

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_residual_ae` 📖	mathematical	—	`Disjoint` `Filter` `Real` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `residual` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`Filter.disjoint_of_disjoint_of_mem` `MeasureTheory.Measure.instOuterMeasureClass` `disjoint_compl_right` `eventually_residual_liouville` `ae_not_liouville`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_not_liouville` 📖	mathematical	—	`Filter.Eventually` `Real` `Liouville` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`Filter.Eventually.mono` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ae_not_liouvilleWith` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Liouville.liouvilleWith`
`ae_not_liouvilleWith` 📖	mathematical	—	`Filter.Eventually` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `Set.setOf_exists` `volume_iUnion_setOf_liouvilleWith`
`setOf_liouvilleWith_subset_aux` 📖	mathematical	—	`Set` `Real` `Set.instHasSubset` `setOf` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `LiouvilleWith` `Set.iUnion` `Set.preimage` `Real.instAdd` `Real.instIntCast` `Filter.Frequently` `Finset` `Finset.instMembership` `Finset.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instPow` `Filter.atTop` `Nat.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_nat_one_div_lt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.Frequently.mono` `Filter.Frequently.and_eventually` `LiouvilleWith.frequently_lt_rpow_neg` `lt_sub_iff_add_lt'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Filter.eventually_ge_atTop` `Nat.one_le_cast` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `LT.lt.trans_le` `zero_lt_one` `NeZero.charZero_one` `Nat.cast_succ` `one_div` `Real.rpow_neg` `Nat.cast_nonneg` `Real.instIsOrderedRing` `one_div_le_one_div_of_le` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_one` `Real.rpow_le_rpow_of_exponent_le` `LE.le.trans` `one_le_two` `Nat.cast_add` `Nat.cast_one` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `LT.lt.le` `Nat.cast_add_one_pos` `Finset.mem_Icc` `neg_lt_iff_pos_add` `Int.instAddLeftMono` `add_comm` `Int.cast_lt` `Int.cast_neg` `Int.cast_one` `Int.cast_add` `Int.cast_natCast` `lt_of_le_of_lt` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `contravariant_swap_add_of_contravariant_add` `mul_nonneg` `IsOrderedRing.toPosMulMono` `sub_lt_iff_lt_add'` `sub_lt_iff_lt_add` `abs_sub_lt_iff` `div_lt_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `abs_of_pos` `abs_div` `sub_div'` `LT.lt.ne'` `add_le_add_iff_left` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `zero_add` `LiouvilleWith.add_int`
`volume_iUnion_setOf_liouvilleWith` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.iUnion` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `setOf` `LiouvilleWith` `instZeroENNReal`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `setOf_liouvilleWith_subset_aux` `MeasureTheory.measure_iUnion_null_iff` `instCountableInt` `MeasureTheory.measure_preimage_add_right` `ContinuousAdd.measurableAdd` `Real.borelSpace` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `MeasureTheory.measure_biUnion_null_iff` `Set.to_countable` `SetCoe.countable` `instCountableNat` `one_div` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `LT.lt.trans_le` `zero_lt_one` `Nat.instZeroLEOneClass` `MeasureTheory.measure_setOf_frequently_eq_zero` `Set.setOf_exists` `Set.iUnion_congr_Prop` `Real.volume_ball` `mul_one_div` `NNReal.coe_two` `NNReal.coe_natCast` `NNReal.coe_rpow` `NNReal.coe_div` `ENNReal.ofReal_coe_nnreal` `MeasureTheory.measure_biUnion_finset_le` `Finset.sum_congr` `Finset.sum_const` `Int.card_Icc` `sub_zero` `nsmul_eq_mul` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `neg_eq_zero` `sub_eq_zero_of_eq` `div_eq_mul_inv` `add_mul` `Distrib.rightDistribClass` `one_mul` `NNReal.rpow_sub'` `NNReal.rpow_one` `NNReal.rpow_neg` `mul_add` `Distrib.leftDistribClass` `mul_left_comm` `ne_top_of_le_ne_top` `ENNReal.tsum_coe_ne_top_iff_summable` `Summable.mul_left` `NNReal.instIsTopologicalSemiring` `Summable.add` `lt_of_not_ge` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `ENNReal.tsum_le_tsum`
`volume_setOf_liouville` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `setOf` `Liouville` `instZeroENNReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ae_not_liouville`

---

← Back to Index