Zulip Chat Archive

I want to make a structure for Lipschitz continuity over functions ℝⁿ -> ℝ. the definition is valid for any norm, so I want to make the kind of norm (Euclidian, Manhattan, etc.) a parameter for the structure.

so far I have something like this:

structure LipschitzContinuous
    (f : ℝ → ℝ)
    (norm : Norm ℝ)
    where
    L : Real
    h : ∀ x y : ℝ, |(f y) - (f x)| ≤ L * norm (y - x)

(there are a handful of things wrong with this code but) mainly I'm not sure how to specify an arbitrary norm here. any help appreciated, thanks!

Luigi Massacci (Mar 07 2025 at 06:59):

You can look at docs#LipschitzWith, but really, I would double down on my suggestion from another thread. You should just read #mil, it will have explanations for all these things

Becker A. (Mar 08 2025 at 21:45):

thanks for the recs. I ended up writing my own somewhat as an exercise:

structure LipschitzContinuous
    [Field ℝ] [Lattice ℝ]
    {ℝn : Type*} [NormedAddCommGroup ℝn] [NormedSpace ℝ ℝn]
    (f : ℝn → ℝ)
    where
    L : NNReal
    h : ∀ x y : ℝn, abs ((f y) - (f x)) ≤ L * dist y x

Becker A. (Mar 08 2025 at 21:47):

however, even after reading the source for LipschitzWith and also searching through MIL (here and here), it's not clear to me how norms work exactly.

e.g., I want to write an expression for Holder's Inequality, which requires that I have two specific norms: L-p and L-q. how do I force an arbitrary type to have both norms, and be able to specify each one independently? (I see WithLp, but it looks like it only generates a norm by an explicit cross-product of two types; I imagine I'd have to do n-1 cross-products to construct the R^n type with each norm)