Commit 2025-01-28 10:27 20c785e9

View on Github →

chore: use ‖x‖ₑ instead of ↑‖x‖₊ (#20806) Rename lemmas from _nnnorm_/_ennnorm_ to _enorm_ where applicable. Rewrite/golf proofs where necessary.

Estimated changes

modified theorem div_le_egauge_ball
modified theorem div_le_egauge_closedBall
modified theorem egauge_le_of_mem_smul
modified theorem egauge_le_of_smul_mem
modified theorem egauge_le_of_smul_mem_of_ne
modified theorem egauge_lt_iff
modified theorem le_egauge_ball_one
modified theorem le_egauge_closedBall_one
modified theorem le_egauge_iff
deleted theorem Real.ennnorm_eq_ofReal
added theorem Real.enorm_eq_ofReal
deleted theorem Real.ofReal_le_ennnorm
added theorem Real.ofReal_le_enorm
deleted theorem edist_eq_coe_nnnorm'
deleted theorem edist_eq_coe_nnnorm_div
added theorem edist_eq_enorm_div
added theorem edist_one_eq_enorm
modified theorem edist_one_right
modified theorem mem_emetric_ball_one_iff
added theorem ofReal_norm_eq_enorm'
deleted theorem AEMeasurable.ennnorm
deleted theorem AEMeasurable.nnnorm
deleted theorem Measurable.ennnorm
deleted theorem Measurable.nnnorm
deleted theorem measurable_ennnorm
added theorem measurable_enorm
modified theorem MeasureTheory.L1.norm_def