Lp space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the space Lp E p μ as the subtype of elements of α →ₘ[μ] E (see ae_eq_fun) such that snorm f p μ is finite. For 1 ≤ p, snorm defines a norm and Lp is a complete metric space.

Main definitions #

• Lp E p μ : elements of α →ₘ[μ] E (see ae_eq_fun) such that snorm f p μ is finite. Defined as an add_subgroup of α →ₘ[μ] E.

Lipschitz functions vanishing at zero act by composition on Lp. We define this action, and prove that it is continuous. In particular,

• continuous_linear_map.comp_Lp defines the action on Lp of a continuous linear map.
• Lp.pos_part is the positive part of an Lp function.
• Lp.neg_part is the negative part of an Lp function.

When α is a topological space equipped with a finite Borel measure, there is a bounded linear map from the normed space of bounded continuous functions (α →ᵇ E) to Lp E p μ. We construct this as bounded_continuous_function.to_Lp.

Notations #

• α →₁[μ] E : the type Lp E 1 μ.
• α →₂[μ] E : the type Lp E 2 μ.

Implementation #

Since Lp is defined as an add_subgroup, dot notation does not work. Use Lp.measurable f to say that the coercion of f to a genuine function is measurable, instead of the non-working f.measurable.

To prove that two Lp elements are equal, it suffices to show that their coercions to functions coincide almost everywhere (this is registered as an ext rule). This can often be done using filter_upwards. For instance, a proof from first principles that f + (g + h) = (f + g) + h could read (in the Lp namespace)

example (f g h : Lp E p μ) : (f + g) + h = f + (g + h) :=
begin
  ext1,
  filter_upwards [coe_fn_add (f + g) h, coe_fn_add f g, coe_fn_add f (g + h), coe_fn_add g h]
    with _ ha1 ha2 ha3 ha4,
  simp only [ha1, ha2, ha3, ha4, add_assoc],
end

The lemma coe_fn_add states that the coercion of f + g coincides almost everywhere with the sum of the coercions of f and g. All such lemmas use coe_fn in their name, to distinguish the function coercion from the coercion to almost everywhere defined functions.

Lp space #

The space of equivalence classes of measurable functions for which snorm f p μ < ∞.

Indicator of a set as an element of Lᵖ #

For a set s with (hs : measurable_set s) and (hμs : μ s < ∞), we build indicator_const_Lp p hs hμs c, the element of Lp corresponding to s.indicator (λ x, c).

Composition on L^p #

We show that Lipschitz functions vanishing at zero act by composition on L^p, and specialize this to the composition with continuous linear maps, and to the definition of the positive part of an L^p function.