The forced regularized mild equation

The forced mild equation eq:reg-mild-forced with values in real spatial L²: the heat evolution of the datum, minus the Stokes Duhamel integral of the regularized tensor, plus the heat Duhamel integral of the Leray projection of the force. The right-hand side is the real part of the inverse transform of its frequency form forcedFourierMild.

noncomputable def CKN.Leray.forcedForceSlice (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : ↥RealVectorL2

The spatial L² class of a time slice of a force, set to zero at the times where the slice is not square integrable.

Equations

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

noncomputable def CKN.Leray.forcedHeatLeray (τ : ℝ) (hτ : 0 ≤ τ) (v : ↥RealVectorL2) : ↥RealVectorL2

The heat evolution of the Leray projection, S(τ) ℙ, on real L².

Equations

• CKN.Leray.forcedHeatLeray τ hτ v = CKN.Leray.realPartVectorL2 (CKN.Leray.heatSemigroup τ hτ (CKN.Leray.lerayProjectionL2 (CKN.Leray.complexifyVectorL2 v)))

noncomputable def CKN.Leray.forcedForceIntegrand (h : ℝ → ↥RealVectorL2) (t s : ℝ) : ↥RealVectorL2

The force Duhamel integrand of eq:reg-mild-forced.

Equations

• CKN.Leray.forcedForceIntegrand h t s = if hs : s ≤ t then CKN.Leray.forcedHeatLeray (t - s) ⋯ (h s) else 0

noncomputable def CKN.Leray.forcedForceDuhamel (h : ℝ → ↥RealVectorL2) (t : ℝ) : ↥RealVectorL2

The force Duhamel integral ∫₀ᵗ S(t-s) ℙ f(s) ds of eq:reg-mild-forced.

Equations

• CKN.Leray.forcedForceDuhamel h t = ∫ (s : ℝ) in Set.Ioc 0 t, CKN.Leray.forcedForceIntegrand h t s

noncomputable def CKN.Leray.forcedMildRHS (b : ↥RealVectorL2) (h : ℝ → ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (t : ℝ) (ht : 0 ≤ t) : ↥RealVectorL2

The right-hand side of the forced mild equation eq:reg-mild-forced for a datum, a force curve and a tensor curve.

Equations

• CKN.Leray.forcedMildRHS b h F t ht = CKN.Leray.realHeatOperator t ht b - CKN.Leray.regularizedMildStokesIntegral F t + CKN.Leray.forcedForceDuhamel h t

noncomputable def CKN.Leray.forcedRealInverse : ↥ComplexVectorL2 →L[ℝ] ↥RealVectorL2

The real part of the inverse transform, as a real continuous linear map.

Equations

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

theorem CKN.Leray.forcedRealInverse_apply (w : ↥ComplexVectorL2) : forcedRealInverse w = realPartVectorL2 ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3).symm w)

theorem CKN.Leray.forcedRealInverse_stokesIntegrand (F : ℝ → ↥RealTensorL2) (t s : ℝ) : forcedRealInverse (forcedFourierStokesIntegrand (fun (r : ℝ) => (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 (F r))) t s) = regularizedMildStokesIntegrand F t s

The frequency form of the Stokes integrand inverts to the real Stokes integrand.

theorem CKN.Leray.forcedRealInverse_forceIntegrand (h : ℝ → ↥RealVectorL2) (t s : ℝ) : forcedRealInverse (forcedFourierForceIntegrand (fun (r : ℝ) => (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 (h r))) t s) = forcedForceIntegrand h t s

The frequency form of the force integrand inverts to the real force integrand.

theorem CKN.Leray.forcedRealInverse_heat (b : ↥RealVectorL2) (t : ℝ) (ht : 0 ≤ t) : forcedRealInverse (heatMultiplier t ht • (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 b)) = realHeatOperator t ht b

The heat evolution is the inverse of its frequency form.

noncomputable def CKN.Leray.forcedFourierTensorCurve (F : ℝ → ↥RealTensorL2) (s : ℝ) : ↥ComplexTensorL2

The transformed tensor curve.

Equations

• CKN.Leray.forcedFourierTensorCurve F s = (MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexTensor3) (CKN.Leray.complexifyTensorL2 (F s))

noncomputable def CKN.Leray.forcedFourierForceCurve (h : ℝ → ↥RealVectorL2) (s : ℝ) : ↥ComplexVectorL2

The transformed force curve.

Equations

• CKN.Leray.forcedFourierForceCurve h s = (MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3) (CKN.Leray.complexifyVectorL2 (h s))

theorem CKN.Leray.stronglyMeasurable_forcedFourierTensorCurve {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) : MeasureTheory.StronglyMeasurable (forcedFourierTensorCurve F)

theorem CKN.Leray.stronglyMeasurable_forcedFourierForceCurve {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) : MeasureTheory.StronglyMeasurable (forcedFourierForceCurve h)

theorem CKN.Leray.norm_forcedFourierTensorCurve_le (F : ℝ → ↥RealTensorL2) (s : ℝ) : ‖forcedFourierTensorCurve F s‖ ≤ ‖F s‖

theorem CKN.Leray.norm_forcedFourierForceCurve_le (h : ℝ → ↥RealVectorL2) (s : ℝ) : ‖forcedFourierForceCurve h s‖ ≤ ‖h s‖

theorem CKN.Leray.integrableOn_forcedFourier_integrands {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) {t C : ℝ} (ht : 0 ≤ t) (hFC : ∀ s ∈ Set.Ioc 0 t, ‖F s‖ ≤ C) (hH : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 t) MeasureTheory.volume) : MeasureTheory.IntegrableOn (forcedFourierStokesIntegrand (forcedFourierTensorCurve F) t) (Set.Ioc 0 t) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (forcedFourierForceIntegrand (forcedFourierForceCurve h) t) (Set.Ioc 0 t) MeasureTheory.volume

Integrability of the frequency Duhamel integrands of the forced mild equation, for a bounded tensor curve and an integrable force curve.

theorem CKN.Leray.forcedMildRHS_eq_forcedRealInverse (b : ↥RealVectorL2) {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) {t C : ℝ} (ht : 0 ≤ t) (hFC : ∀ s ∈ Set.Ioc 0 t, ‖F s‖ ≤ C) (hH : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 t) MeasureTheory.volume) : forcedMildRHS b h F t ht = forcedRealInverse (forcedFourierMild ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 b)) (forcedFourierTensorCurve F) (forcedFourierForceCurve h) t ht)

The right-hand side of the forced mild equation is the real part of the inverse transform of its frequency form.