Commit 2026-03-30 20:46 8807830d

View on Github →

feat: add missing API for lp E p (#35152) The API for lp is significantly underdeveloped. This PR attempts to rectify some of the shortcomings. In particular, we provide:

  • some missing tools for Memℓp, notably memℓp_norm_iff and Memℓp.mono.
  • some improved docstrings and more uniform notation for the non-dependent case; note that we also remove the notation ℓ^∞(ι) for lp (fun _ : ι ↦ ℝ) ∞ on the basis that there are other choices besides ℝ which would make at least as much sense here, including ℂ.
  • bundled version of maps (evaluation, inclusion as a linear map, summation in ℓ¹) as well as cleaning-up a few other odds and ends.

Estimated changes

modified theorem LipschitzOnWith.coordinate
modified theorem LipschitzWith.coordinate
added theorem Memℓp.mono'
added theorem Memℓp.mono
added def lp.evalCLM
added def lp.evalₗ
added def lp.linearMapOfLE
added theorem lp.linearMapOfLE_comp
added theorem lp.norm_mono
added theorem lp.norm_toNorm
added theorem lp.norm_tsum_le
added def lp.toNorm
added theorem lp.zeroBasis_apply
added theorem memℓp_gen_iff''
added theorem memℓp_gen_iff'
added theorem memℓp_norm_iff
modified def kuratowskiEmbedding