Commit 2026-03-06 09:14 58db26d5

View on Github →

feat: lemmas about Measure.count (#36205)

Also add some gcongr attributes for Real.toENNReal. Used for Sobolev spaces

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/ENatENNReal.lean

Created Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean

added theorem MeasureTheory.eLpNorm_count_lt_top

added theorem MeasureTheory.eLpNorm_count_lt_top_of_lt

added theorem MeasureTheory.eLpNorm_dirac

added theorem MeasureTheory.enorm_le_eLpNorm_count

Modified Mathlib/MeasureTheory/Measure/Count.lean

added theorem Function.Injective.map_count_le

added theorem Subsingleton.count_eq_dirac

added theorem Unique.count_eq_dirac