Pairings of the force pressure with fixed test functions

For a fixed function ψ ∈ L^{6/5}, the pairing f ↦ ∫ p_f ψ of the slice force pressure of lem:force-pressure is a bounded linear functional on spatial L². By the Riesz representation theorem it is the pairing with one fixed L² field, which is what makes the force pressure measurable in time.

theorem CKN.Leray.forcePressure_integrable_mul {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (v : ↥RealVectorL2) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => forcePressureSlice v x * ψ x) MeasureTheory.volume

theorem CKN.Leray.forcePressure_pairing_bound {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (v : ↥RealVectorL2) : ‖∫ (x : Foundation.Parabolic.Vec3), forcePressureSlice v x * ψ x‖ ≤ (gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume).toReal * 2 * ‖v‖

noncomputable def CKN.Leray.forcePressurePairing (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : StrongDual ℝ ↥RealVectorL2

The pairing of the slice force pressure with a fixed L^{6/5} function, as a bounded linear functional on spatial L².

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.forcePressurePairingField (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : ↥RealVectorL2

The Riesz representative of the pairing functional of the slice force pressure.

Equations

• CKN.Leray.forcePressurePairingField ψ hψ = (InnerProductSpace.toDual ℝ ↥CKN.Leray.RealVectorL2).symm (CKN.Leray.forcePressurePairing ψ hψ)

theorem CKN.Leray.integral_forcePressureSlice_mul_eq (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (v : ↥RealVectorL2) : ∫ (x : Foundation.Parabolic.Vec3), forcePressureSlice v x * ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, realVectorL2Representative (forcePressurePairingField ψ hψ) x i * realVectorL2Representative v x i

The pairing of the slice force pressure with a fixed L^{6/5} function is the L² pairing of the input field with the Riesz representative.