Commit 2023-11-10 17:28 f3ca3380

feat(LiminfLimsup, LpSeminorm): add lemmas/golf (#8300)

• Add blimsup_eq_limsup and bliminf_eq_liminf
• Generalize limsup_nat_add and liminf_nat_add to a ConditionallyCompleteLattice.
• Add Filter.HasBasis.blimsup_eq_iInf_iSup.
• Add limsup_sup_filter, liminf_sup_filter, blimsup_sup_not, bliminf_inf_not, blimsup_not_sup, bliminf_not_inf, limsup_piecewise, and liminf_piecewise.
• Add essSup_piecewise.
• Assume that the codomain is ℝ≥0∞ in essSup_indicator_eq_essSup_restrict. This allows us to drop assumptions 0 ≤ᵐ[_] f and μ s ≠ 0.
• Upgrade inequality to an equality in snormEssSup_piecewise_le (now snormEssSup_piecewise) and snorm_top_piecewise_le (now snorm_top_piecewise).
• Use new lemmas to golf some proofs.