Commit 2025-10-16 08:57 acf42d31

View on Github →

feat(Topology): Add PairReduction.lean (#26243) Add file PairReduction.lean which proves the theorem pair_reduction which is needed for the proof of the general Kolmogorov-Chentsov theorem in the Brownian Motion project.

depends on: #27239

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/EMetricSpace/PairReduction.lean

added theorem EMetric.pair_reduction

added theorem PairReduction.antitone_logSizeBallSeq_add_one_subset

added theorem PairReduction.card_finset_logSizeBallSeq_add_one_lt

added theorem PairReduction.card_finset_logSizeBallSeq_card_eq_zero

added theorem PairReduction.card_finset_logSizeBallSeq_le

added theorem PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius

added theorem PairReduction.card_pairSetSeq_le_logSizeRadius_mul

added theorem PairReduction.card_pairSet_le

added theorem PairReduction.disjoint_smallBall_logSizeBallSeq

added theorem PairReduction.edist_le_of_mem_pairSet

added theorem PairReduction.exists_radius_le

added theorem PairReduction.finset_logSizeBallSeq_add_one

added theorem PairReduction.finset_logSizeBallSeq_add_one_ssubset

added theorem PairReduction.finset_logSizeBallSeq_add_one_subset

added theorem PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init

added theorem PairReduction.finset_logSizeBallSeq_zero

added theorem PairReduction.iSup_edist_pairSet

added def PairReduction.logSizeBallSeq

added def PairReduction.logSizeBallStruct.ball

added def PairReduction.logSizeBallStruct.smallBall

added structure PairReduction.logSizeBallStruct

added def PairReduction.logSizeRadius

added theorem PairReduction.logSizeRadius_le_card_smallBall

added theorem PairReduction.one_le_logSizeRadius

added theorem PairReduction.one_le_radius_logSizeBallSeq

added def PairReduction.pairSet

added def PairReduction.pairSetSeq

added theorem PairReduction.pairSet_empty_eq_empty

added theorem PairReduction.pairSet_subset

added theorem PairReduction.point_logSizeBallSeq_add_one

added theorem PairReduction.point_logSizeBallSeq_zero

added theorem PairReduction.point_mem_finset_logSizeBallSeq

added theorem PairReduction.point_mem_logSizeBallSeq_init

added theorem PairReduction.point_notMem_finset_logSizeBallSeq_add_one

added theorem PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius

added theorem PairReduction.radius_logSizeBallSeq_add_one

added theorem PairReduction.radius_logSizeBallSeq_le

added theorem PairReduction.radius_logSizeBallSeq_zero

Modified docs/references.bib