Weak gradients from the Fourier transform

For a complex L² field v whose frequency gradient 2πi ξ ⊗ v̂ is square integrable, the inverse transform of that tensor is the weak gradient of v. Its real part is the weak gradient of the real part of v, and its squared L² norm is the frequency dissipation ∫ 4π²|ξ|²|v̂|². This identifies the dissipation of the energy identity of lem:regularised-forced with the Dirichlet energy of the solution.

noncomputable def CKN.Leray.forcedFourierGradHat (v : ↥ComplexVectorL2) (ξ : Foundation.Parabolic.L2Vec3) : ComplexTensor3

The frequency gradient (2πi ξᵢ v̂ⱼ)ᵢⱼ of a complex L² field.

Equations

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

theorem CKN.Leray.norm_sq_forcedFourierGradHat (v : ↥ComplexVectorL2) (ξ : Foundation.Parabolic.L2Vec3) : ‖forcedFourierGradHat v ξ‖ ^ 2 = forcedFourierLam ξ * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) ξ‖ ^ 2

theorem CKN.Leray.measurable_forcedFourierGradHat (v : ↥ComplexVectorL2) : Measurable (forcedFourierGradHat v)

noncomputable def CKN.Leray.forcedFourierGrad (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) : ↥ComplexTensorL2

The inverse transform of the frequency gradient.

Equations

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

theorem CKN.Leray.norm_sq_forcedFourierGrad (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) : ‖forcedFourierGrad v hv‖ ^ 2 = ∫ (ξ : Foundation.Parabolic.L2Vec3), forcedFourierLam ξ * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) ξ‖ ^ 2

theorem CKN.Leray.inner_toLp_single_one (j : Fin 3) (w : ComplexVec3) : inner ℂ (WithLp.toLp 2 (Pi.single j 1)) w = w.ofLp j

noncomputable def CKN.Leray.complexVecSlot (j : Fin 3) : ℂ →L[ℂ] ComplexVec3

The continuous linear map placing a scalar in the jth slot of a complex three-vector.

Equations

• CKN.Leray.complexVecSlot j = (ContinuousLinearMap.id ℂ ℂ).smulRight (WithLp.toLp 2 (Pi.single j 1))

noncomputable def CKN.Leray.complexTensorSlot (i j : Fin 3) : ℂ →L[ℂ] ComplexTensor3

The continuous linear map placing a scalar in the (i, j) slot of a complex three-by-three tensor.

Equations

• CKN.Leray.complexTensorSlot i j = (ContinuousLinearMap.id ℂ ℂ).smulRight (WithLp.toLp 2 (Pi.single i (WithLp.toLp 2 (Pi.single j 1))))

theorem CKN.Leray.inner_complexVecSlot (j : Fin 3) (a : ℂ) (w : ComplexVec3) : inner ℂ ((complexVecSlot j) a) w = (starRingEnd ℂ) a * w.ofLp j

theorem CKN.Leray.inner_complexTensorSlot (i j : Fin 3) (a : ℂ) (T : ComplexTensor3) : inner ℂ ((complexTensorSlot i j) a) T = (starRingEnd ℂ) a * (T.ofLp i).ofLp j

theorem CKN.Leray.schwartz_lineDerivOp_postcompCLM {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) (f : SchwartzMap Foundation.Parabolic.L2Vec3 F) (m : Foundation.Parabolic.L2Vec3) : LineDeriv.lineDerivOp m ((SchwartzMap.postcompCLM L) f) = (SchwartzMap.postcompCLM L) (LineDeriv.lineDerivOp m f)

Line derivatives of Schwartz maps commute with real-linear postcomposition.

theorem CKN.Leray.inner_toLp_basisVec (ξ : Foundation.Parabolic.L2Vec3) (i : Fin 3) : inner ℝ ξ (WithLp.toLp 2 (basisVec i)) = ξ.ofLp i

theorem CKN.Leray.inner_vecSlot_freqGrad (i j : Fin 3) (a : ℂ) (w : ComplexVec3) (ξ : Foundation.Parabolic.L2Vec3) : inner ℂ ((complexVecSlot j) (2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp i) * a)) w = -inner ℂ ((complexTensorSlot i j) a) (WithLp.toLp 2 fun (k : Fin 3) => (2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp k)) • w)

The frequency identity behind the weak derivative: the pairing of a differentiated slot vector with w is minus the pairing of the slot tensor with the frequency gradient of w.

theorem CKN.Leray.fourier_vecSlot_lineDeriv (i j : Fin 3) (φC : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) (ξ : Foundation.Parabolic.L2Vec3) : (FourierTransform.fourier ((SchwartzMap.postcompCLM (complexVecSlot j)) (LineDeriv.lineDerivOp (WithLp.toLp 2 (basisVec i)) φC))) ξ = (complexVecSlot j) (2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp i) * (FourierTransform.fourier φC) ξ)

The transform of a differentiated slot test vector.

theorem CKN.Leray.fourier_tensorSlot (i j : Fin 3) (φC : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) (ξ : Foundation.Parabolic.L2Vec3) : (FourierTransform.fourier ((SchwartzMap.postcompCLM (complexTensorSlot i j)) φC)) ξ = (complexTensorSlot i j) ((FourierTransform.fourier φC) ξ)

The transform of a slot test tensor.

theorem CKN.Leray.forcedFourierGrad_inner_test (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (i j : Fin 3) (φC : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) : inner ℂ (((SchwartzMap.postcompCLM (complexVecSlot j)) (LineDeriv.lineDerivOp (WithLp.toLp 2 (basisVec i)) φC)).toLp 2 MeasureTheory.volume) v = -inner ℂ (((SchwartzMap.postcompCLM (complexTensorSlot i j)) φC).toLp 2 MeasureTheory.volume) (forcedFourierGrad v hv)

Plancherel for a differentiated vector test field against a field with square-integrable frequency gradient.

theorem CKN.Leray.re_inner_vecSlot_test (w : ↥ComplexVectorL2) (j : Fin 3) (φL : SchwartzMap Foundation.Parabolic.L2Vec3 ℝ) : (inner ℂ (((SchwartzMap.postcompCLM (complexVecSlot j)) ((SchwartzMap.postcompCLM Complex.ofRealCLM) φL)).toLp 2 MeasureTheory.volume) w).re = ∫ (y : Foundation.Parabolic.L2Vec3), φL y * ((↑↑w y).ofLp j).re

The real part of the pairing of a slot test field with a complex vector field is the integral against the real part of that component.

theorem CKN.Leray.re_inner_tensorSlot_test (G : ↥ComplexTensorL2) (i j : Fin 3) (φL : SchwartzMap Foundation.Parabolic.L2Vec3 ℝ) : (inner ℂ (((SchwartzMap.postcompCLM (complexTensorSlot i j)) ((SchwartzMap.postcompCLM Complex.ofRealCLM) φL)).toLp 2 MeasureTheory.volume) G).re = ∫ (y : Foundation.Parabolic.L2Vec3), φL y * (((↑↑G y).ofLp i).ofLp j).re

The real part of the pairing of a slot test tensor with a complex tensor field is the integral against the real part of that entry.

theorem CKN.Leray.forcedFourierGrad_hasWeakPartialDerivOn (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (i j : Fin 3) : HasWeakPartialDerivOn Set.univ i (fun (x : Vec 3) => ((↑↑v (WithLp.toLp 2 x)).ofLp j).re) fun (x : Vec 3) => (((↑↑(forcedFourierGrad v hv) (WithLp.toLp 2 x)).ofLp i).ofLp j).re

The real part of a complex L² field has, as weak partial derivatives, the real parts of the inverse transform of its frequency gradient.