Pairing with a density

The pairing f ↦ ∑ e, f e * η e of a density η : Density E against real-valued functions f : E → ℝ, bundled as a continuous linear functional (an element of StrongDual ℝ (E → ℝ)). Assembling it from already-bundled pieces (ContinuousLinearMap.proj, scalar multiples, sums) makes linearity and continuity automatic.

For strictly positive η the pairing is coercive on nonnegative functions: a bound η.pairing f ≤ c forces the coordinatewise bound f e ≤ c / η e. Consequently the sublevel sets of the pairing over Density.toReal '' Γ.Adm are compact — the hypothesis needed to apply the minimum-at-an-extreme-point machinery of LeanModulus.Common.ExtremePoints in the duality argument.

noncomputable def Density.pairing {E : Type u_1} [Fintype E] (η : Density E) : StrongDual ℝ (E → ℝ)

The pairing f ↦ ∑ e, f e * η e of the density η against real-valued functions, as a continuous linear functional on E → ℝ.

Equations

• η.pairing = ∑ e : E, ↑(η e) • ContinuousLinearMap.proj e

@[simp]

theorem Density.pairing_apply {E : Type u_1} [Fintype E] (η : Density E) (f : E → ℝ) : η.pairing f = ∑ e : E, f e * ↑(η e)

theorem Density.pairing_toReal_eq_length {E : Type u_1} [Fintype E] (η ρ : Density E) : η.pairing ρ.toReal = ↑(η.length ρ)

Pairing η against the coercion of a density ρ computes the ℝ≥0-valued length η.length ρ, coerced to ℝ. This bridges the real-analysis side (pairing) back to the ℝ≥0 admissibility language of LeanModulus.Common.FamilyOfObjects.

theorem Density.apply_le_div_of_pairing_le {E : Type u_1} [Fintype E] (η : Density E) (f : E → ℝ) (c : ℝ) (h : η.pairing f ≤ c) (hpos : ∀ (e : E), 0 < η e) (hf : ∀ (e : E), 0 ≤ f e) (e : E) : f e ≤ c / ↑(η e)

If a nonnegative function f pairs against a strictly positive density η to at most c, then each coordinate satisfies f e ≤ c / η e. This is the coercivity estimate that traps sublevel sets of the pairing in a compact box.

theorem FamilyOfObjects.isCompact_sublevel_toReal_image_adm {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) (η : Density E) (hη : ∀ (e : E), 0 < η e) (c : ℝ) : IsCompact {f : E → ℝ | f ∈ Density.toReal '' Γ.Adm ∧ η.pairing f ≤ c}

Sublevel sets of the pairing with a strictly positive density η, taken within the image of the admissible set, are compact: they are closed and trapped in the box ∏ e, [0, c / η e] by the coercivity estimate Density.apply_le_div_of_pairing_le.