Commit 2025-11-05 17:51 e5cab449

View on Github →

chore: turn WithLp into a structure (#27270) Turn WithLp into a one field structure, as was suggested many times on Zulip and discussed here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/526234806. Here is what this PR does:

  • The instances on WithLp p α which were defeq to those on α (algebraic instances, topology, uniformity, bornology) are now pulled back from α along WithLp.equiv p α. A few declarations are added to ease the process, such as versions of WithLp.equiv as a homeomorphism or a uniform isomorphism.
  • The MeasurableSpace structure was pushed forward from α. We now make it pulled back because it is much more convenient to prove that this preserves the BorelSpace instance.
  • It introduces some definitions to equip α × β with the Lp distance, and similarly for Π i, α i. This is then used to define relevant instances on type synonyms, such as for matrix norms.
  • The PR fixes all the defeq abuses (which break obviously).

Estimated changes

modified theorem WithLp.measurable_ofLp
modified theorem WithLp.measurable_toLp
deleted theorem PiLp.ofLp_apply
modified theorem PiLp.toLp_apply
modified def WithLp.idemFst
modified theorem WithLp.idemFst_apply
modified def WithLp.idemSnd
modified theorem WithLp.idemSnd_apply
modified theorem WithLp.prod_continuous_ofLp
modified theorem WithLp.prod_continuous_toLp
added def WithLp.delabToLp
deleted def WithLp.ofLp
modified theorem WithLp.ofLp_eq_zero
modified theorem WithLp.ofLp_toLp
deleted def WithLp.toLp
modified theorem WithLp.toLp_eq_zero
added structure WithLp
deleted def WithLp