BesicovitchVectorSpace

📁 Source: Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

Statistics

Metric	Count
Definitions centerAndRescale, goodδ, goodτ, multiplicity	4
Theorems centerAndRescale_center, centerAndRescale_radius, exists_normalized, exists_normalized_aux1, exists_normalized_aux2, exists_normalized_aux3, card_le_multiplicity, card_le_multiplicity_of_δ, card_le_of_separated, exists_goodδ, goodδ_lt_one, instHasBesicovitchCovering, isEmpty_satelliteConfig_multiplicity, le_multiplicity_of_δ_of_fin, multiplicity_le, one_lt_goodτ	16
Total	20

Besicovitch

Definitions

Name	Category	Theorems
goodδ 📖	CompOp	1 math math: goodδ_lt_one
goodτ 📖	CompOp	2 math math: isEmpty_satelliteConfig_multiplicity, one_lt_goodτ
multiplicity 📖	CompOp	6 math math: le_multiplicity_of_δ_of_fin, card_le_multiplicity_of_δ, exists_goodδ, isEmpty_satelliteConfig_multiplicity, card_le_multiplicity, multiplicity_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le_multiplicity 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	Finset.card multiplicity	—	Nat.instAtLeastTwoHAddOfNat le_csSup card_le_of_separated
card_le_multiplicity_of_δ 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne goodδ SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	Finset.card multiplicity	—	Nat.instAtLeastTwoHAddOfNat exists_goodδ
card_le_of_separated 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	Finset.card Monoid.toNatPow Nat.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	—	Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup locallyCompact_of_proper FiniteDimensional.proper_real Mathlib.Meta.NormNum.isNNRat_lt_true Real.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Metric.ball_disjoint_ball dist_eq_norm Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Nat.cast_one Set.iUnion₂_subset Metric.ball_subset_ball' dist_zero_right add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_rfl Mathlib.Meta.NormNum.isNNRat_eq_true MeasureTheory.measure_biUnion_finset measurableSet_ball BorelSpace.opensMeasurable Finset.sum_congr MeasureTheory.Measure.addHaar_ball_of_pos MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure mul_assoc Finset.sum_const nsmul_eq_mul MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass ENNReal.mul_le_mul_iff_left LT.lt.ne' Metric.measure_ball_pos MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one LT.lt.ne MeasureTheory.measure_ball_lt_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ENNReal.toReal_le_of_le_ofReal pow_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le div_eq_mul_inv one_mul inv_pow ENNReal.ofReal_inv_of_pos IsStrictOrderedRing.toPosMulStrictMono Real.instNontrivial ENNReal.ofReal_pow ENNReal.ofReal_ofNat ENNReal.toReal_mul ENNReal.toReal_natCast ENNReal.toReal_inv ENNReal.toReal_pow ENNReal.toReal_ofNat mul_pow IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE
exists_goodδ 📖	mathematical	—	Real Real.instLT Real.instZero Real.instOne Finset.card multiplicity	—	Nat.instAtLeastTwoHAddOfNat lt_or_ge Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq Fintype.card_fin Function.Embedding.exists_of_card_le_finset Function.Embedding.injective norm_zero Real.instIsOrderedRing sub_self covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace dist_zero_right pi_norm_le_iff_of_nonneg zero_le_two Real.instZeroLEOneClass IsCompact.tendsto_subseq TopologicalSpace.instFirstCountableTopologyForallOfCountable instCountableFin ProperSpace.isCompact_closedBall pi_properSpace FiniteDimensional.proper_real Filter.Tendsto.norm Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.apply_nhds instIsTopologicalAddGroupReal tendsto_const_nhds Filter.Tendsto.comp StrictMono.tendsto_atTop le_of_tendsto_of_tendsto' HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat sub_zero lt_irrefl LE.le.trans_lt zero_lt_one NeZero.charZero_one RCLike.charZero_rclike Finset.card_image_of_injective Finset.card_fin card_le_multiplicity LT.lt.trans_le AddTorsor.nonempty Function.sometimes_spec
goodδ_lt_one 📖	mathematical	—	Real Real.instLT goodδ Real.instOne	—	Nat.instAtLeastTwoHAddOfNat exists_goodδ
instHasBesicovitchCovering 📖	mathematical	—	HasBesicovitchCovering NormedAddCommGroup.toMetricSpace	—	one_lt_goodτ isEmpty_satelliteConfig_multiplicity
isEmpty_satelliteConfig_multiplicity 📖	mathematical	—	IsEmpty SatelliteConfig NormedAddCommGroup.toMetricSpace multiplicity goodτ	—	Nat.instAtLeastTwoHAddOfNat SatelliteConfig.exists_normalized SatelliteConfig.centerAndRescale_center SatelliteConfig.centerAndRescale_radius LT.lt.le one_lt_goodτ le_rfl goodδ_lt_one lt_irrefl LT.lt.trans_le le_multiplicity_of_δ_of_fin
le_multiplicity_of_δ_of_fin 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Pairwise Real.instSub Real.instOne goodδ SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	multiplicity	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing sub_self norm_zero Mathlib.Tactic.Linarith.sub_neg_of_lt goodδ_lt_one Finset.card_image_of_injective Finset.card_fin card_le_multiplicity_of_δ
multiplicity_le 📖	mathematical	—	multiplicity Monoid.toNatPow Nat.instMonoid Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	—	csSup_le instIsEmptyFalse card_le_of_separated
one_lt_goodτ 📖	mathematical	—	Real Real.instLT Real.instOne goodτ	—	lt_of_not_ge exists_goodδ Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike 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

Besicovitch.SatelliteConfig

Definitions

Name	Category	Theorems
centerAndRescale 📖	CompOp	2 math math: centerAndRescale_radius, centerAndRescale_center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centerAndRescale_center 📖	mathematical	—	c NormedAddCommGroup.toMetricSpace centerAndRescale NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	sub_self smul_zero
centerAndRescale_radius 📖	mathematical	—	r NormedAddCommGroup.toMetricSpace centerAndRescale Real Real.instOne	—	inv_mul_cancel₀ LT.lt.ne' rpos
exists_normalized 📖	mathematical	c NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup r Real Real.instOne Real.instLE Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Norm.norm NormedAddCommGroup.toNorm Pairwise Real.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat div_zero zero_smul norm_zero Real.instIsOrderedRing norm_smul NormedSpace.toNormSMulClass norm_div Real.norm_ofNat norm_norm IsUnit.div_mul_cancel le_or_gt LE.le.trans exists_normalized_aux1 exists_normalized_aux2 exists_normalized_aux3 norm_sub_rev le_of_not_ge
exists_normalized_aux1 📖	mathematical	r NormedAddCommGroup.toMetricSpace Real Real.instOne Real.instLE Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instSub Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup c	—	Nat.instAtLeastTwoHAddOfNat dist_eq_norm h le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow sq_nonneg AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono Mathlib.Tactic.Ring.add_overlap_pf inv_eq_one_div le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_le_iff₀ mul_comm hlast' le_trans norm_sub_rev Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_mul Mathlib.Tactic.Linarith.without_one_mul
exists_normalized_aux2 📖	mathematical	c NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup r Real Real.instOne Real.instLE Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Norm.norm NormedAddCommGroup.toNorm Real.instLT	Real.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	Nat.instAtLeastTwoHAddOfNat dist_eq_norm h le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one dist_zero_right inter' lt_or_ge LE.le.trans hlast sub_zero top_le_iff one_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow sq_nonneg AddGroup.existsAddOfLE norm_sub_rev Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.add_nonpos le_of_lt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isRat_le_true sub_le_sub_left covariant_swap_add_of_covariant_add mul_le_of_le_one_left mul_assoc rpos one_mul add_le_add_right div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LE.le.trans_lt zero_le_two LT.lt.le one_smul sub_smul norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs abs_of_nonneg sub_mul Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono IsStrictOrderedRing.toPosMulStrictMono PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ 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.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₁ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt lt_trans zero_lt_one NeZero.one GroupWithZero.toNontrivial
exists_normalized_aux3 📖	mathematical	c NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup r Real Real.instOne Real.instLE Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instLT Norm.norm NormedAddCommGroup.toNorm	Real.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	Nat.instAtLeastTwoHAddOfNat dist_eq_norm h le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul dist_zero_right inter' lt_top_iff_ne_top lt_irrefl LE.le.trans_lt zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_zero sub_zero hlast LT.lt.trans_le LT.lt.trans zero_lt_two NeZero.charZero_one one_smul AddRightCancelSemigroup.toIsRightCancelAdd sub_smul norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs abs_of_nonneg sub_nonneg covariant_swap_add_of_covariant_add div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono one_mul sub_mul div_mul_cancel₀ LT.lt.ne' sub_nonpos mul_nonneg IsOrderedRing.toPosMulMono LT.lt.le sub_le_sub norm_sub_rev Mathlib.Tactic.Ring.mul_pf_left mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono mul_le_mul_of_nonneg_left Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono LE.le.trans Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_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.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ 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 Mathlib.Meta.NormNum.isNat_eq_false ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Linarith.add_neg CancelDenoms.mul_subst smul_sub smul_smul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero

---

← Back to Index