Documentation Verification Report

Uniform

📁 Source: Mathlib/Analysis/Convex/Uniform.lean

Statistics

Metric	Count
Definitions `UniformConvexSpace`	1
Theorems `toStrictConvexSpace`, `uniform_convex`, `exists_forall_closed_ball_dist_add_le_two_mul_sub`, `exists_forall_closed_ball_dist_add_le_two_sub`, `exists_forall_sphere_dist_add_le_two_sub`	5
Total	6

UniformConvexSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toStrictConvexSpace` 📖	mathematical	—	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`StrictConvexSpace.of_norm_add_ne_two` `Nat.instAtLeastTwoHAddOfNat` `exists_forall_closed_ball_dist_add_le_two_sub` `norm_sub_pos_iff` `LT.lt.ne` `LE.le.trans_lt` `Eq.le` `le_rfl` `sub_lt_self` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`uniform_convex` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	—

(root)

Definitions

Name	Category	Theorems
`UniformConvexSpace` 📖	CompData	2 math math: `InnerProductSpace.toUniformConvexSpace`, `InnerProductSpaceable.to_uniformConvexSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_forall_closed_ball_dist_add_le_two_mul_sub` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instSub` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LT.lt.not_ge` `LE.le.trans` `norm_sub_le` `add_nonpos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `exists_forall_closed_ball_dist_add_le_two_sub` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_pos` `norm_smul_of_nonneg` `inv_nonneg` `LT.lt.le` `div_eq_inv_mul` `div_le_one` `sub_mul` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `div_le_div_iff_of_pos_right`
`exists_forall_closed_ball_dist_add_le_two_sub` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_three` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `exists_forall_sphere_dist_add_le_two_sub` `lt_min` `one_half_pos` `le_or_gt` `one_add_one_eq_two` `LE.le.trans` `norm_add_le_of_le` `Eq.le` `sub_add_eq_add_sub` `Eq.ge` `add_sub_assoc` `sub_pos_of_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `min_lt_of_left_lt` `one_half_lt_one` `norm_smul_of_nonneg` `inv_nonneg` `norm_nonneg` `inv_mul_cancel₀` `LT.lt.ne'` `LT.lt.trans` `one_smul` `sub_smul` `sub_nonneg_of_le` `one_le_inv₀` `LT.lt.trans_le` `sub_mul` `one_mul` `sub_le_comm` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `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.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `sub_le_sub` `add_le_add` `LT.lt.le` `min_le_of_right_le` `min_le_left` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isInt_neg` `add_zero` `Mathlib.Tactic.Abel.zero_termg` `sub_le_iff_le_add` `norm_sub_rev` `add_assoc` `norm_add₃_le` `min_le_right` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Nat.cast_one` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_neg_of_lt`
`exists_forall_sphere_dist_add_le_two_sub` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`UniformConvexSpace.uniform_convex`

---

← Back to Index