ℒp space and Lp space #

This file describes properties of almost everywhere strongly measurable functions with finite seminorm, denoted by snorm f p μ and defined for p:ℝ≥0∞ asmm_group (Lp E p μ) := 0 if p=0, (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and ess_sup ‖f‖ μ for p=∞.

The Prop-valued mem_ℒp f p μ states that a function f : α → E has finite seminorm. The space Lp E p μ is 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 #

• snorm' f p μ : (∫ ‖f a‖^p ∂μ) ^ (1/p) for f : α → F and p : ℝ, where α is a measurable space and F is a normed group.

• snorm_ess_sup f μ : seminorm in ℒ∞, equal to the essential supremum ess_sup ‖f‖ μ.

• snorm f p μ : for p : ℝ≥0∞, seminorm in ℒp, equal to 0 for p=0, to snorm' f p μ for 0 < p < ∞ and to snorm_ess_sup f μ for p = ∞.

• mem_ℒp f p μ : property that the function f is almost everywhere strongly measurable and has finite p-seminorm for the measure μ (snorm f p μ < ∞)

• 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.

ℒp seminorm #

We define the ℒp seminorm, denoted by snorm f p μ. For real p, it is given by an integral formula (for which we use the notation snorm' f p μ), and for p = ∞ it is the essential supremum (for which we use the notation snorm_ess_sup f μ).

We also define a predicate mem_ℒp f p μ, requesting that a function is almost everywhere measurable and has finite snorm f p μ.

This paragraph is devoted to the basic properties of these definitions. It is constructed as follows: for a given property, we prove it for snorm' and snorm_ess_sup when it makes sense, deduce it for snorm, and translate it in terms of mem_ℒp.