Compactness Gradient Projection #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.weak_l2_compLpL
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
{μ : MeasureTheory.Measure α}
(L : E →L[ℝ] F)
(f : ℕ → ↥(MeasureTheory.Lp E 2 μ))
(g : ↥(MeasureTheory.Lp E 2 μ))
(hweak :
∀ (w : ↥(MeasureTheory.Lp E 2 μ)), Filter.Tendsto (fun (k : ℕ) => inner ℝ (f k) w) Filter.atTop (nhds (inner ℝ g w)))
(w : ↥(MeasureTheory.Lp F 2 μ))
:
Filter.Tendsto (fun (k : ℕ) => inner ℝ (L.compLp (f k)) w) Filter.atTop (nhds (inner ℝ (L.compLp g) w))
Weak convergence in Hilbert-valued L² is preserved by a continuous
linear map of the fibers.
theorem
CKN.Leray.weak_l2_scalar_integral_of_fiber_weak
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure α}
(L : E →L[ℝ] ℝ)
(F : ℕ → α → E)
(G : ↥(MeasureTheory.Lp E 2 μ))
(hF : ∀ (k : ℕ), MeasureTheory.MemLp (F k) 2 μ)
(hweak :
∀ (v : ↥(MeasureTheory.Lp E 2 μ)),
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (F k) ⋯) v) Filter.atTop (nhds (inner ℝ G v)))
(w : α → ℝ)
(hw : MeasureTheory.MemLp w 2 μ)
:
Applying a scalar functional to a weakly convergent L² sequence gives
convergence of its integrals against every scalar L² test.
Evaluation of one matrix entry is continuous on the Euclidean gradient fiber.
Equations
- CKN.Leray.gradientCoordinateCLM i j = PiLp.proj 2 (fun (x : Fin 3) => ℝ) j ∘SL PiLp.proj 2 (fun (x : Fin 3) => CKN.Foundation.Parabolic.L2Vec3) i
Instances For
@[simp]
theorem
CKN.Leray.gradientCoordinateCLM_toCompactnessGradientFiber
(i j : Fin 3)
(A : Fin 3 → Foundation.Parabolic.Vec3)
: