The forced energy inequality in the limit

These are the energy steps in the proof of thm:leray-forced. The energy inequality eq:reg-energy-forced of each forced regularized solution is put in real form; the work term converges by strong L² convergence, the kinetic energy and the dissipation are weakly lower semicontinuous, and the limit satisfies the forced energy inequality (FLH2). Its small-time form and weak continuity at 0 give the strong initial trace (LH5).

theorem CKN.Leray.forcedHopf_norm_toLp_sq {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (g x)) ⋯‖ ^ 2 = ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), g x i ^ 2

The square of the L² norm of a Euclidean field is the sum of its coordinate square integrals.

theorem CKN.Leray.forcedHopf_dissipation_eq_ofReal (U : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t₀ : ℝ) (hD : MeasureTheory.MemLp D 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))) : regUniformDissipation U D t₀ = ENNReal.ofReal (∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), D z i j ^ 2)

The dissipation of a field with a square-integrable weak gradient on the slab (0,t) is the sum of the coordinate square integrals.

theorem CKN.Leray.forcedHopf_energy_real_of_regularised (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (U f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t₀ : ℝ) (hslice : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => U (x, t₀)) 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp D 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))) (henergy : (MeasureTheory.eLpNorm (regUniformVelocitySlice U t₀) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation U D t₀).toReal ≤ (MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2).toReal + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ i : Fin 3, f z i * U z i) : (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), U (x, t₀) i ^ 2) + 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), D z i j ^ 2 ≤ (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ i : Fin 3, f z i * U z i

The energy inequality eq:reg-energy-forced of a forced regularized solution at a positive time, in real form, with the mollified datum bounded by the datum.

theorem CKN.Leray.forcedHopf_energy_limit_real (t₀ : ℝ) (Useq : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dseq : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (R : ℕ → ℝ) (Rlim : ℝ) (hUn : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Useq n (x, t₀)) 2 MeasureTheory.volume) (hu : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t₀)) 2 MeasureTheory.volume) (hweak : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, Useq n (x, t₀) i * u (x, t₀) i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t₀) i * u (x, t₀) i))) (hDn : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => Dseq n z i j) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))) (hDweak : ∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Dseq n z i j * Du z i j) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Du z i j * Du z i j))) (hEn : ∀ (n : ℕ), (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), Useq n (x, t₀) i ^ 2) + 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Dseq n z i j ^ 2 ≤ R n) (hR : Filter.Tendsto R Filter.atTop (nhds Rlim)) : (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u (x, t₀) i ^ 2) + 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Du z i j ^ 2 ≤ Rlim

Weak lower semicontinuity of the kinetic energy and the dissipation: if the approximating energies are bounded by convergent real numbers, the limit energy is bounded by their limit.

theorem CKN.Leray.forcedHopf_energy_ennreal (t₀ : ℝ) (u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t₀)) 2 MeasureTheory.volume) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (hreal : (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u (x, t₀) i ^ 2) + 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Du z i j ^ 2 ≤ (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ i : Fin 3, f z i * u z i) : (ENNReal.ofReal (1 / 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t₀))) ^ 2) + ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ENNReal.ofReal (spatialGradientSq u Du z) < ⊤ ∧ ((ENNReal.ofReal (1 / 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t₀))) ^ 2) + ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ENNReal.ofReal (spatialGradientSq u Du z)).toReal ≤ (ENNReal.ofReal (1 / 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2).toReal + ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ i : Fin 3, f z i * u z i

The real forced energy inequality gives the energy clause (FLH2) at a positive time.

theorem CKN.Leray.forcedHopf_initialTrace (T : ℝ) (hT : 0 < T) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hu0 : ∀ (x : Foundation.Parabolic.Vec3), u (x, 0) = a x) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (hslice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (e : ℝ → ℝ) (he : Filter.Tendsto e (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (henergy : ∀ (t : ℝ), 0 < t → t ≤ T → ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u (x, t) i ^ 2 ≤ (∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + e t) (hcont : ContinuousOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * a x i) (Set.Icc 0 T)) : Filter.Tendsto (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t) - a x)) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The strong initial trace (LH5) from weak continuity at 0 and an energy bound whose excess over the initial energy vanishes as t ↓ 0.

theorem CKN.Leray.forcedHopf_work_tendsto {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hmeas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (U n) μ) (hu : MeasureTheory.MemLp u 2 μ) (hf : MeasureTheory.MemLp f 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, f z i * U n z i ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, f z i * u z i ∂μ))

The work pairings converge under strong L² convergence of the velocities; the approximations are square integrable from some index on.

theorem CKN.Leray.forcedHopf_exists_bound_of_eventually_le {x : ℕ → ℝ} {B : ℝ} (h : ∀ᶠ (n : ℕ) in Filter.atTop, x n ≤ B) : ∃ (B' : ℝ), 0 ≤ B' ∧ ∀ (n : ℕ), x n ≤ B'

A real sequence bounded from some index on is bounded.