Time differentiation through the Leray projection

The L² Fourier construction of the Leray projection is a bounded linear map. This file records the curve-calculus consequence used when differentiating the projected evolution equation (prop:lps-smoothing).

@[instance_reducible]

def ESS.LPS.smoothingTimeRegularityPointNormedAddCommGroup : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

Gives space-time points the product normed additive group structure for smoothing.

Equations

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

@[instance_reducible]

noncomputable def ESS.LPS.smoothingTimeRegularityPointNormedSpace : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

Gives space-time points the product real normed space structure for smoothing.

Equations

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

theorem ESS.LPS.lps_strong_solution_weak_equation_of_divFree_test {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsLpsStrongSolution t₀ t₁ u Du p) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ t₁)) (hdiv : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0

The strong weak equation is pressure-free when tested against a smooth compactly supported solenoidal field (prop:lps-smoothing).

theorem ESS.LPS.lps_strong_solution_full_weak_equation_D2 {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsLpsStrongSolution t₀ t₁ u Du p) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ t₁)) : ∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁), ∑ i : Fin 3, Dtu z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - ∑ i : Fin 3, ∑ j : Fin 3, D2u z i j j * φ z i - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

Integrating the strong weak equation by parts in time and space gives its full pressure-inclusive distribution identity (prop:lps-smoothing). The time derivative and Laplacian are the specified weak derivatives from IsLpsStrongSolution.

noncomputable def ESS.LPS.lerayFourierMultiplierLinear : ↥(MeasureTheory.Lp CKN.Leray.ComplexVec3 2 MeasureTheory.volume) →ₗ[ℂ] ↥(MeasureTheory.Lp CKN.Leray.ComplexVec3 2 MeasureTheory.volume)

The complex Leray multiplier on frequency-space L² is linear.

Equations

• ESS.LPS.lerayFourierMultiplierLinear = { toFun := CKN.Leray.lerayFourierMultiplier, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ESS.LPS.lerayProjectionL2CLM : ↥CKN.Leray.ComplexVectorL2 →L[ℂ] ↥CKN.Leray.ComplexVectorL2

The complex physical-space Leray projection as a continuous linear map.

Equations

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

noncomputable def ESS.LPS.realLerayProjectionCLM : ↥CKN.Leray.RealVectorL2 →L[ℝ] ↥CKN.Leray.RealVectorL2

The real Leray projection is a continuous linear map on spatial L².

Equations

• ESS.LPS.realLerayProjectionCLM = CKN.Leray.realPartVectorL2 ∘SL ContinuousLinearMap.restrictScalars ℝ ESS.LPS.lerayProjectionL2CLM ∘SL CKN.Leray.complexifyVectorL2

theorem ESS.LPS.realLerayProjectionCLM_apply (f : ↥CKN.Leray.RealVectorL2) : realLerayProjectionCLM f = CKN.Leray.realLerayProjection f

The continuous linear realization agrees with the real Leray projection used in the Fourier construction.

theorem ESS.LPS.realLerayProjectionCLM_norm_le (f : ↥CKN.Leray.RealVectorL2) : ‖realLerayProjectionCLM f‖ ≤ ‖f‖

The real Leray projection contracts the spatial L² norm.

theorem ESS.LPS.realLerayProjectionCLM_eq_self_of_isWeakDivFree (f : ↥CKN.Leray.RealVectorL2) (hf : CKN.IsWeakDivFreeL2 (CKN.Leray.realVectorL2Representative f)) : realLerayProjectionCLM f = f

The Leray projection fixes every spatial L² field whose representative is weakly divergence-free (prop:lps-smoothing).

theorem ESS.LPS.lps_strong_solution_slice_projection_eq {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsLpsStrongSolution t₀ t₁ u Du p) {t : ℝ} (ht : t ∈ Set.Icc t₀ t₁) : have hSlice := ⋯; realLerayProjectionCLM (CKN.Leray.realVectorL2OfCoordinateFunction (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) hSlice) = CKN.Leray.realVectorL2OfCoordinateFunction (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) hSlice

Every strong-solution time slice is fixed by the Leray projection in spatial L² (prop:lps-smoothing).

theorem ESS.LPS.realLerayProjection_orderedL2_energy_le (m : ℕ) (F : List (Fin 3) → ↥CKN.Leray.RealVectorL2) : ∑ α ∈ CKN.sobolevWords m, ‖realLerayProjectionCLM (F α)‖ ^ 2 ≤ ∑ α ∈ CKN.sobolevWords m, ‖F α‖ ^ 2

Applying the Leray projection in each ordered derivative slot does not increase the finite H^m sum of spatial L² norms (prop:lps-smoothing). Identifying these slots with the weak derivatives of the projected field is the separate distributional commutation step.

@[reducible, inline]

abbrev ESS.LPS.OrderedSpatialL2Family (m : ℕ) : Type

The finite product of spatial L² slots through ordered derivative degree m.

Equations

• ESS.LPS.OrderedSpatialL2Family m = PiLp 2 fun (x : ↥(CKN.sobolevWords m)) => ↥CKN.Leray.RealVectorL2

noncomputable def ESS.LPS.realLerayProjectionOrderedLinear (m : ℕ) : OrderedSpatialL2Family m →ₗ[ℝ] OrderedSpatialL2Family m

Apply the Leray multiplier in each ordered spatial L² slot through degree m.

Equations

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

noncomputable def ESS.LPS.realLerayProjectionOrderedCLM (m : ℕ) : OrderedSpatialL2Family m →L[ℝ] OrderedSpatialL2Family m

The Leray multiplier is a contraction on the finite ordered integer H^m product of spatial L² slots (prop:lps-smoothing). This bound is the operator estimate used after identifying the projected slots with weak derivatives.

Equations

• ESS.LPS.realLerayProjectionOrderedCLM m = (ESS.LPS.realLerayProjectionOrderedLinear m).mkContinuous 1 ⋯

theorem ESS.LPS.realLerayProjectionOrderedCLM_apply (m : ℕ) (F : OrderedSpatialL2Family m) (α : ↥(CKN.sobolevWords m)) : ((realLerayProjectionOrderedCLM m) F).ofLp α = realLerayProjectionCLM (F.ofLp α)

The ordered Sobolev multiplier is linear slotwise.

theorem ESS.LPS.realLerayProjectionOrderedCLM_norm_le (m : ℕ) (F : OrderedSpatialL2Family m) : ‖(realLerayProjectionOrderedCLM m) F‖ ≤ ‖F‖

The Leray multiplier does not increase the ordered integer H^m norm (prop:lps-smoothing).