Lower semicontinuity of nonlinear integrals along L² approximations #
If finitely many sequences converge in L² and a continuous nonnegative function of their values
has integrals eventually bounded by K, then the same function of the limits has integral at most
K. This transfers the smooth nonlinear estimates of the bootstrap of thm:vorticity-regularity
to the weak fields.
theorem
ESS.vorticity_integral_le_of_L2_tendsto
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[Finite ι]
{a : ι → ℕ → α → ℝ}
{A : ι → α → ℝ}
(ha : ∀ (i : ι) (n : ℕ), MeasureTheory.MemLp (a i n) 2 μ)
(hA : ∀ (i : ι), MeasureTheory.MemLp (A i) 2 μ)
(hconv : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (a i n - A i) 2 μ) Filter.atTop (nhds 0))
{H : (ι → ℝ) → ℝ}
(hH : Continuous H)
(hH0 : ∀ (v : ι → ℝ), 0 ≤ H v)
(hint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : α) => H fun (i : ι) => a i n x) μ)
{K : ℝ}
(hK : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (x : α), H fun (i : ι) => a i n x ∂μ ≤ K)
:
Fatou's lemma for a continuous nonnegative function of finitely many L²-convergent
sequences.