Commit 2023-03-10 06:37 d88a041c

View on Github →

feat: port Topology.Instances.ENNReal (#2734) API changes:

  • Add HasSum.sum_range_add, sum_add_tsum_nat_add', and tsum_eq_zero_add'. We had these (or stronger) results for topological groups. These versions works for monoids.
  • Rename tendsto_atTop_csupr to tendsto_atTop_csupᵢ, tendsto_atBot_csupr to tendsto_atBot_csupᵢ, tendsto_atBot_cinfi to tendsto_atBot_cinfᵢ, and tendsto_atTop_cinfi to tendsto_atTop_cinfᵢ.
  • Add a shortcut instance for T5Space ENNReal.
  • Add ENNReal.nhdsWithin_Ioi_one_neBot, ENNReal.nhdsWithin_Ioi_nat_neBot, ENNReal.nhdsWithin_Ioi_ofNat_nebot, and ENNReal.nhdsWithin_Iio_neBot.
  • Add ENNReal.hasBasis_nhds_of_ne_top and ENNReal.hasBasis_nhds_of_ne_top'.
  • Add ENNReal.binfᵢ_le_nhds and ENNReal.tendsto_nhds_of_Icc.
  • Use Real.nnabs instead of nnnorm to avoid dependency on analysis.normed.group.basic (forward-port of leanprover-community/mathlib#18562).
  • Add ENNReal.tsum_eq_limsup_sum_nat.
  • Add ENNReal.tsum_comp_le_tsum_of_injective, ENNReal.tsum_le_tsum_comp_of_surjective, use them to golf some proofs.
  • Add ENNReal.tsum_bunionᵢ_le_tsum, ENNReal.tsum_unionᵢ_le_tsum. We had versions of these lemmas for finite collections. The proofs for infinite collections are simpler. Most of these changes were done to fix some long proofs: it was easier for me (@urkud) to add supporting lemmas and golf the proof than to fix the original code.

Estimated changes

added theorem HasSum.sum_range_add
added theorem sum_add_tsum_nat_add'
added theorem tsum_eq_zero_add'
deleted theorem tendsto_atBot_cinfi
added theorem tendsto_atBot_cinfᵢ
deleted theorem tendsto_atBot_csupr
added theorem tendsto_atBot_csupᵢ
deleted theorem tendsto_atTop_cinfi
added theorem tendsto_atTop_cinfᵢ
deleted theorem tendsto_atTop_csupr
added theorem tendsto_atTop_csupᵢ
added theorem Continuous.edist
added theorem Continuous.ennreal_mul
added theorem EMetric.diam_closure
added theorem EMetric.isClosed_ball
added theorem ENNReal.Icc_mem_nhds
added theorem ENNReal.add_bsupᵢ'
added theorem ENNReal.add_bsupᵢ
added theorem ENNReal.add_supᵢ
added theorem ENNReal.bsupᵢ_add'
added theorem ENNReal.bsupᵢ_add
added theorem ENNReal.continuous_coe
added theorem ENNReal.continuous_pow
added theorem ENNReal.embedding_coe
added theorem ENNReal.hasSum_lt
added theorem ENNReal.hasSum_toReal
added theorem ENNReal.inv_liminf
added theorem ENNReal.inv_limsup
added theorem ENNReal.inv_map_infᵢ
added theorem ENNReal.inv_map_supᵢ
added theorem ENNReal.isOpen_ne_top
added theorem ENNReal.mul_supᵢ
added theorem ENNReal.mul_supₛ
added theorem ENNReal.nhds_coe
added theorem ENNReal.nhds_coe_coe
added theorem ENNReal.nhds_of_ne_top
added theorem ENNReal.nhds_top'
added theorem ENNReal.nhds_top
added theorem ENNReal.nhds_top_basis
added theorem ENNReal.nhds_zero
added theorem ENNReal.sub_supᵢ
added theorem ENNReal.supᵢ_add
added theorem ENNReal.supᵢ_div
added theorem ENNReal.supᵢ_mul
added theorem ENNReal.supₛ_add
added theorem ENNReal.tendsto_coe
added theorem ENNReal.tendsto_ofReal
added theorem ENNReal.tendsto_sub
added theorem ENNReal.tendsto_toReal
added theorem ENNReal.tsum_lt_tsum
added theorem ENNReal.tsum_sub
added theorem ENNReal.tsum_supᵢ_eq
added theorem ENNReal.tsum_toReal_eq
added theorem ENNReal.tsum_union_le
added theorem Filter.Tendsto.edist
added theorem Metric.diam_closure
added theorem NNReal.summable_of_le
added theorem NNReal.summable_sigma
added theorem NNReal.tsum_lt_tsum
added theorem NNReal.tsum_pos
added theorem Real.diam_Icc
added theorem Real.diam_Ico
added theorem Real.diam_Ioc
added theorem Real.diam_Ioo
added theorem Real.diam_eq
added theorem Real.ediam_Icc
added theorem Real.ediam_Ico
added theorem Real.ediam_Ioc
added theorem Real.ediam_Ioo
added theorem Real.ediam_eq
added theorem Summable.toNNReal
added theorem continuous_edist
added theorem summable_of_sum_le
added theorem tsum_lt_tsum_of_nonneg