Division estimates in ℝ≥0∞

For a ≤ b in ℝ≥0∞ the difference 1 - a / b lies in [0, 1], and it is read in ℝ as 1 - a.toReal / b.toReal; when a < b it is positive. With a = n the dimension and b = p an integrability exponent, this is the Hölder exponent 1 - n / p of Morrey's embedding, which is 1 for p = ∞.

The file also records exhaustion of an extended nonnegative function by its positive level sets, and the absorption step of elliptic estimates: a finite quantity bounded by b plus half of itself is at most 2 b.

Main declarations

• ENNReal.toReal_one_sub_div: (1 - a / b).toReal = 1 - a.toReal / b.toReal for a ≤ b.
• ENNReal.one_sub_one_div_toReal_nonneg: for 1 ≤ p, the Hölder exponent 1 - 1 / p.toReal is nonnegative.
• ENNReal.toNNReal_one_sub_div_pos: 0 < (1 - a / b).toNNReal for a < b.
• ENNReal.exists_nnreal_two_le_inv_sub_lt_and_inv_add_le_one: for r > 1 and n > 0 with n (2 - r) < 2 r, a finite exponent t ≥ 2 with 1/2 - 1/t < 1/n and 1/r + 1/t ≤ 1.
• ENNReal.exists_inv_lt_inv_add_inv_two_and_inv_add_inv_le_iff: for 0 < q < 2, an exponent s with q⁻¹ < s⁻¹ + 2⁻¹ and p⁻¹ + s⁻¹ ≤ q⁻¹ exists exactly when 2 < p.
• ENNReal.le_mul_two_of_le_add_div_two: the absorption step a ≤ b + a / 2 → a ≤ 2 b for finite a, as used in elliptic estimates.
• ENNReal.ofReal_pow_div_natCast_div_mul_ofReal_natCast_mul: the cancellation ofReal (d ^ n / n) / m * ofReal (n * a) = ofReal (a * d ^ n / m.toReal) for m finite and nonzero.

theorem ENNReal.monotone_indicator_inv_natCast_add_one_le {X : Type u_1} (f : X → ENNReal) : Monotone fun (n : ℕ) => {x : X | (↑n + 1)⁻¹ ≤ f x}.indicator f

Restricting a nonnegative function to the levels above 1 / (n + 1) is monotone in n.

theorem ENNReal.iSup_indicator_inv_natCast_add_one_le {X : Type u_1} (f : X → ENNReal) : (fun (x : X) => ⨆ (n : ℕ), {x : X | (↑n + 1)⁻¹ ≤ f x}.indicator f x) = f

The restrictions to the levels above 1 / (n + 1) exhaust any nonnegative function.

@[simp]

theorem ENNReal.toReal_one_sub_div {a b : ENNReal} (hab : a ≤ b) : (1 - a / b).toReal = 1 - a.toReal / b.toReal

For a ≤ b, the difference 1 - a / b is read in ℝ as 1 - a.toReal / b.toReal.

theorem ENNReal.toNNReal_one_sub_div_pos {a b : ENNReal} (hab : a < b) : 0 < (1 - a / b).toNNReal

For a < b, the difference 1 - a / b is positive, even after truncation to ℝ≥0.

theorem ENNReal.one_sub_one_div_toReal_nonneg {p : ENNReal} (hp : 1 ≤ p) : 0 ≤ 1 - 1 / p.toReal

For 1 ≤ p, the Hölder exponent 1 - 1 / p is nonnegative (with p = ∞ giving 1).

theorem ENNReal.le_mul_two_of_le_add_div_two {a b : ENNReal} (ha : a ≠ ⊤) (h : a ≤ b + a / 2) : a ≤ b * 2

Absorption: a finite quantity bounded by b plus half of itself is at most 2 b.

theorem ENNReal.exists_nnreal_two_le_inv_sub_lt_and_inv_add_le_one {n : ℝ} (hn : 0 < n) {r : NNReal} (hr : 1 < r) (hrn : n * (2 - ↑r) < 2 * ↑r) : ∃ (t : NNReal), 0 < t ∧ 2 ≤ ↑t ∧ 2⁻¹ - (↑t)⁻¹ < n⁻¹ ∧ (↑r)⁻¹ + (↑t)⁻¹ ≤ 1

A finite exponent t ≥ 2 complementing r. For n > 0 and r > 1 with n (2 - r) < 2 r, there is a finite exponent t ≥ 2 with 1/2 - 1/t < 1/n and 1/r + 1/t ≤ 1: take 1/t = min (1/2) (1 - 1/r).

theorem ENNReal.exists_inv_lt_inv_add_inv_two_and_inv_add_inv_le_iff {p q : ENNReal} (hq0 : q ≠ 0) (hq2 : q < 2) : (∃ (s : ENNReal), q⁻¹ < s⁻¹ + 2⁻¹ ∧ p⁻¹ + s⁻¹ ≤ q⁻¹) ↔ 2 < p

For 0 < q < 2, an exponent s with q⁻¹ < s⁻¹ + 2⁻¹ and p⁻¹ + s⁻¹ ≤ q⁻¹ exists exactly when 2 < p: at p = 2 the two conditions would force q⁻¹ < q⁻¹.

This is the exponent bookkeeping for the compactness of multiplication by α ∈ L^p from W^{1,q} to L^q in dimension two, for 1 < q < 2 on a compact surface or a bounded domain with Lipschitz boundary (the local form of McDuff–Salamon, J-holomorphic Curves and Symplectic Topology, Lemma C.2.2). There W^{1,q} embeds compactly in L^s for every s below the Sobolev exponent 2q/(2-q), that is for q⁻¹ < s⁻¹ + 2⁻¹, and Hölder's inequality on the finite measure space maps L^p × L^s to L^q when p⁻¹ + s⁻¹ ≤ q⁻¹. The arithmetic itself needs neither a domain nor 1 < q.

theorem ENNReal.ofReal_pow_div_natCast_div_mul_ofReal_natCast_mul {n : ℕ} {d a : ℝ} {m : ENNReal} (hn : 0 < n) (hd : 0 ≤ d) (hm₀ : m ≠ 0) (hm_top : m ≠ ⊤) : ENNReal.ofReal (d ^ n / ↑n) / m * ENNReal.ofReal (↑n * a) = ENNReal.ofReal (a * d ^ n / m.toReal)

Cancelling a finite nonzero denominator m against the factor n of a product: ofReal (d ^ n / n) / m * ofReal (n * a) = ofReal (a * d ^ n / m).