ENNReal.ofReal of differences and suprema of maxima

For 0 ≤ q ≤ p, the embedding ENNReal.ofReal splits p into p - q and q. With p = 1 and q = θ, this says that the interpolation weights 1 - θ and θ sum to one in ℝ≥0∞.

For a class P of functions α → ℝ, the quantity ⨆ (F : α → ℝ) (_ : P F), ENNReal.ofReal (⨆ x, F x) in ℝ≥0∞ is the supremum of the maxima of the functions in the class. Capacities in symplectic geometry, such as the Hofer–Zehnder capacity and its variants, are defined this way, and their conformality and symplectic invariance reduce to the two facts here: the supremum scales with a rescaling of the class, and it is unchanged by a reparametrization of the class along surjections.

Main results

• TauCeti.ofReal_sub_add_ofReal: ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p for 0 ≤ q ≤ p.
• TauCeti.le_ofReal_inv_add_mul_of_add_le: if a + b ≤ V and b ≥ ω V, then a ≤ (1 + ω)⁻¹ V.
• TauCeti.iSup₂_ofReal_iSup_eq_ofReal_mul: if the class Q consists of the c • F with F in P, for c > 0, then the supremum for Q is c times that for P.
• TauCeti.iSup₂_ofReal_iSup_eq_of_comp: classes related by composition with surjections have the same supremum of maxima.

@[simp]

theorem TauCeti.ofReal_sub_add_ofReal {p q : ℝ} (hq : 0 ≤ q) (hqp : q ≤ p) : ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p

For 0 ≤ q ≤ p, ENNReal.ofReal adds p - q and q back up to p.

theorem TauCeti.le_ofReal_inv_add_mul_of_add_le {a b : ENNReal} {V ω : ℝ} (hV : 0 ≤ V) (hω : 0 ≤ ω) (hb : ENNReal.ofReal (ω * V) ≤ b) (hab : a + b ≤ ENNReal.ofReal V) : a ≤ ENNReal.ofReal (1 + ω)⁻¹ * ENNReal.ofReal V

If a + b ≤ V and b ≥ ω V, then a ≤ (1 + ω)⁻¹ V: the complement of a set filling an ω fraction of a set of measure V fills at most a (1 + ω)⁻¹ fraction of it.

theorem TauCeti.iSup₂_ofReal_iSup_eq_ofReal_mul {α : Type u_1} {P Q : (α → ℝ) → Prop} {c : ℝ} (hc : 0 < c) (h : ∀ (F : α → ℝ), Q (c • F) ↔ P F) : ⨆ (F : α → ℝ), ⨆ (_ : Q F), ENNReal.ofReal (⨆ (x : α), F x) = ENNReal.ofReal c * ⨆ (F : α → ℝ), ⨆ (_ : P F), ENNReal.ofReal (⨆ (x : α), F x)

Rescaling a class of functions. If, for c > 0, the functions satisfying Q are exactly the c • F with F satisfying P, then the supremum of their maxima is c times that for P.

theorem TauCeti.iSup₂_ofReal_iSup_eq_of_comp {α : Type u_1} {β : Type u_2} {P : (α → ℝ) → Prop} {Q : (β → ℝ) → Prop} {f : α → β} {g : β → α} (hf : Function.Surjective f) (hg : Function.Surjective g) (hPQ : ∀ (F : α → ℝ), P F → Q (F ∘ g)) (hQP : ∀ (G : β → ℝ), Q G → P (G ∘ f)) : ⨆ (G : β → ℝ), ⨆ (_ : Q G), ENNReal.ofReal (⨆ (y : β), G y) = ⨆ (F : α → ℝ), ⨆ (_ : P F), ENNReal.ofReal (⨆ (x : α), F x)

Reparametrizing a class of functions. If surjections f : α → β and g : β → α carry the functions satisfying P to functions satisfying Q by F ↦ F ∘ g, and back by G ↦ G ∘ f, then the suprema of the maxima of the two classes agree.