Abstract L² limits along a fast subsequence

A sequence that is Cauchy in L² has a fast subsequence converging almost everywhere; the pointwise limit (chosen by limUnder) is in L² and is the L² limit of the whole sequence. Everything here is stated for an arbitrary measure space.

theorem AVenhance.Infra.FullTheorem.TransportLimit.eLpNorm_two_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) : MeasureTheory.eLpNorm f 2 μ = ENNReal.ofReal √(∫ (a : α), f a ^ 2 ∂μ)

eLpNorm 2 of a square-integrable real function is the square root of its energy.

theorem AVenhance.Infra.FullTheorem.TransportLimit.sqrt_integral_sq_le_of_eLpNorm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) {η : ℝ} (hη : 0 ≤ η) (h : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal η) : √(∫ (a : α), f a ^ 2 ∂μ) ≤ η

A square-integrable function with eLpNorm 2 ≤ ofReal η has energy root at most η.

theorem AVenhance.Infra.FullTheorem.TransportLimit.eLpNorm_le_of_sqrt_integral_sq_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) {η : ℝ} (h : √(∫ (a : α), f a ^ 2 ∂μ) ≤ η) : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal η

Converse: energy root at most η bounds eLpNorm 2.

theorem AVenhance.Infra.FullTheorem.TransportLimit.exists_fast_index (Q : ℕ → ℕ → ℕ → Prop) (h : ∀ (n : ℕ), ∃ (N : ℕ), ∀ j ≥ N, ∀ k ≥ N, Q n j k) : ∃ (s : ℕ → ℕ), Monotone s ∧ (∀ (k : ℕ), k ≤ s k) ∧ ∀ (n a : ℕ), a ≥ n → ∀ b ≥ n, Q n (s a) (s b)

A fast subsequence from a family of ∃ N, ∀ j k ≥ N statements.

theorem AVenhance.Infra.FullTheorem.TransportLimit.tsum_geometric_ne_top : ∑' (i : ℕ), ENNReal.ofReal (2 * (1 / 2) ^ i) ≠ ⊤

Geometric summability in ℝ≥0∞.

theorem AVenhance.Infra.FullTheorem.TransportLimit.ae_tendsto_fast {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} (hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 μ) {s : ℕ → ℕ} (hfast : ∀ (n a : ℕ), a ≥ n → ∀ b ≥ n, MeasureTheory.eLpNorm (f (s a) - f (s b)) 2 μ ≤ ENNReal.ofReal ((1 / 2) ^ n)) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (k : ℕ) => f (s k) x) Filter.atTop (nhds (Filter.atTop.limUnder fun (k : ℕ) => f (s k) x))

A.e. convergence of the fast subsequence.

theorem AVenhance.Infra.FullTheorem.TransportLimit.memLp_limit_of_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {g : α → ℝ} (hf : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (f k) μ) (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (k : ℕ) => f k x) Filter.atTop (nhds (g x))) {c : ENNReal} (hc : c ≠ ⊤) (hb : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (f k) 2 μ ≤ c) : MeasureTheory.MemLp g 2 μ ∧ MeasureTheory.eLpNorm g 2 μ ≤ c

The pointwise limit is in L², and the whole sequence converges to it in L² with the liminf bound.