Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 19:07 2d2929f8

View on Github →

feat(measure_theory): define Hausdorff measure and Hausdorff dimension (#6710)

Estimated changes

Modified docs/references.bib

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.rpow_sub

Modified src/measure_theory/borel_space.lean

added theorem borel_eq_generate_from_is_closed

Created src/measure_theory/hausdorff_measure.lean

added def measure_theory.dimH

added theorem measure_theory.hausdorff_measure_of_dimH_lt

added theorem measure_theory.hausdorff_measure_of_lt_dimH

added def measure_theory.measure.hausdorff_measure

added theorem measure_theory.measure.hausdorff_measure_apply'

added theorem measure_theory.measure.hausdorff_measure_apply

added theorem measure_theory.measure.hausdorff_measure_mono

added theorem measure_theory.measure.hausdorff_measure_zero_or_top

added def measure_theory.measure.mk_metric'

added theorem measure_theory.measure.mk_metric'_to_outer_measure

added def measure_theory.measure.mk_metric

added theorem measure_theory.measure.mk_metric_apply

added theorem measure_theory.measure.mk_metric_mono

added theorem measure_theory.measure.mk_metric_mono_smul

added theorem measure_theory.measure.mk_metric_to_outer_measure

added theorem measure_theory.measure_zero_of_dimH_lt

added theorem measure_theory.outer_measure.coe_mk_metric

added theorem measure_theory.outer_measure.is_metric.borel_le_caratheodory

added theorem measure_theory.outer_measure.is_metric.finset_Union_of_pairwise_separated

added theorem measure_theory.outer_measure.is_metric.le_caratheodory

added def measure_theory.outer_measure.is_metric

added theorem measure_theory.outer_measure.isometric_comap_mk_metric

added theorem measure_theory.outer_measure.isometric_map_mk_metric

added theorem measure_theory.outer_measure.isometry_comap_mk_metric

added theorem measure_theory.outer_measure.isometry_map_mk_metric

added theorem measure_theory.outer_measure.mk_metric'.eq_supr_nat

added theorem measure_theory.outer_measure.mk_metric'.le_pre

added theorem measure_theory.outer_measure.mk_metric'.mono_pre

added theorem measure_theory.outer_measure.mk_metric'.mono_pre_nat

added def measure_theory.outer_measure.mk_metric'.pre

added theorem measure_theory.outer_measure.mk_metric'.pre_le

added theorem measure_theory.outer_measure.mk_metric'.tendsto_pre

added theorem measure_theory.outer_measure.mk_metric'.tendsto_pre_nat

added theorem measure_theory.outer_measure.mk_metric'.trim_pre

added def measure_theory.outer_measure.mk_metric'

added theorem measure_theory.outer_measure.mk_metric'_is_metric

added def measure_theory.outer_measure.mk_metric

added theorem measure_theory.outer_measure.mk_metric_mono

added theorem measure_theory.outer_measure.mk_metric_mono_smul

added theorem measure_theory.outer_measure.trim_mk_metric

Modified src/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.bounded_by_union_of_top_of_nonempty_inter

added theorem measure_theory.outer_measure.comap_bounded_by

added theorem measure_theory.outer_measure.smul_bounded_by

Modified src/topology/separation.lean

added theorem tendsto_nhds_unique_of_eventually_eq