An actual L² realization of the lifted pressure-gradient space on R³ × (R / period Z). The generating vectors are L² representatives of Dφ, for smooth compactly supported scalar test functions φ. Smoothness is expressed through local lifts to R³ × R. The angular measure here has total mass period; renormalizing it changes only a fixed scalar in the L² norm and not the gradient subspace or projection.

@[reducible, inline]

abbrev EulerLiftedGradientSpace.Vector3 : Type

Three dimensional real Euclidean vectors.

Equations

• EulerLiftedGradientSpace.Vector3 = EuclideanSpace ℝ (Fin 3)

@[reducible, inline]

abbrev EulerLiftedGradientSpace.LiftDomain (period : ℝ) : Type

The spatial cylinder with one periodic angle coordinate.

Equations

• EulerLiftedGradientSpace.LiftDomain period = (EulerLiftedGradientSpace.Vector3 × AddCircle period)

@[reducible, inline]

abbrev EulerLiftedGradientSpace.LiftTangent : Type

The four dimensional real covering space of the cylinder.

Equations

• EulerLiftedGradientSpace.LiftTangent = (EulerLiftedGradientSpace.Vector3 × ℝ)

noncomputable def EulerLiftedGradientSpace.liftMeasure (period : ℝ) [Fact (0 < period)] : MeasureTheory.Measure (LiftDomain period)

Product Lebesgue and angle Haar measure on the cylinder.

Equations

• EulerLiftedGradientSpace.liftMeasure period = MeasureTheory.volume.prod MeasureTheory.volume

instance EulerLiftedGradientSpace.liftMeasure_finiteOnCompacts (period : ℝ) [Fact (0 < period)] : MeasureTheory.IsFiniteMeasureOnCompacts (liftMeasure period)

@[reducible, inline]

noncomputable abbrev EulerLiftedGradientSpace.LiftL2 (period : ℝ) [Fact (0 < period)] : AddSubgroup (LiftDomain period →ₘ[liftMeasure period] Vector3)

The genuine Hilbert space of square integrable vector fields on the cylinder.

Equations

• EulerLiftedGradientSpace.LiftL2 period = MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 (EulerLiftedGradientSpace.liftMeasure period)

def EulerLiftedGradientSpace.localLift (period : ℝ) (φ : LiftDomain period → ℝ) (x : LiftDomain period) : LiftTangent → ℝ

The scalar field pulled back to covering coordinates centered at x.

Equations

• EulerLiftedGradientSpace.localLift period φ x h = φ (x.1 + h.1, x.2 + ↑h.2)

def EulerLiftedGradientSpace.coveringMap (period : ℝ) : LiftTangent → LiftDomain period

The quotient covering map from the real tangent space to the cylinder.

Equations

• EulerLiftedGradientSpace.coveringMap period z = (z.1, ↑z.2)

theorem EulerLiftedGradientSpace.coveringMap_isOpenQuotient (period : ℝ) : IsOpenQuotientMap (coveringMap period)

theorem EulerLiftedGradientSpace.localLift_cover (period : ℝ) (φ : LiftDomain period → ℝ) (z : LiftTangent) : localLift period φ (coveringMap period z) = fun (h : LiftTangent) => localLift period φ 0 (z + h)

theorem EulerLiftedGradientSpace.fderiv_localLift_cover (period : ℝ) (φ : LiftDomain period → ℝ) (z : LiftTangent) : fderiv ℝ (localLift period φ (coveringMap period z)) 0 = fderiv ℝ (localLift period φ 0) z

noncomputable def EulerLiftedGradientSpace.liftedGradient (period κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (x : LiftDomain period) : Vector3

The actual differential expression κ ∇_y φ + m ∂_θ φ.

Equations

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

theorem EulerLiftedGradientSpace.liftedGradient_continuous (period κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : Continuous (liftedGradient period κ m φ)

theorem EulerLiftedGradientSpace.liftedGradient_zero_of_notMem_tsupport (period κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (x : LiftDomain period) (hx : x ∉ tsupport φ) : liftedGradient period κ m φ x = 0

theorem EulerLiftedGradientSpace.liftedGradient_hasCompactSupport (period κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ) : HasCompactSupport (liftedGradient period κ m φ)

theorem EulerLiftedGradientSpace.liftedGradient_memLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : MeasureTheory.MemLp (liftedGradient period κ m φ) 2 (liftMeasure period)

Every smooth compact test has an actual L² lifted gradient.

def EulerLiftedGradientSpace.translatedTest (period : ℝ) (a : LiftDomain period) (φ : LiftDomain period → ℝ) : LiftDomain period → ℝ

Translation of a scalar test function on the cylinder.

Equations

• EulerLiftedGradientSpace.translatedTest period a φ x = φ (x + a)

@[simp]

theorem EulerLiftedGradientSpace.localLift_translated (period : ℝ) (a x : LiftDomain period) (φ : LiftDomain period → ℝ) : localLift period (translatedTest period a φ) x = localLift period φ (x + a)

theorem EulerLiftedGradientSpace.smoothCompactTest_translated (period : ℝ) (a : LiftDomain period) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : HasCompactSupport (translatedTest period a φ) ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period (translatedTest period a φ) x)

@[simp]

theorem EulerLiftedGradientSpace.liftedGradient_translated (period κ : ℝ) (m : Vector3) (a x : LiftDomain period) (φ : LiftDomain period → ℝ) : liftedGradient period κ m (translatedTest period a φ) x = liftedGradient period κ m φ (x + a)

theorem EulerLiftedGradientSpace.measurePreserving_translation (period : ℝ) [Fact (0 < period)] (a : LiftDomain period) : MeasureTheory.MeasurePreserving (fun (x : LiftDomain period) => x + a) (liftMeasure period) (liftMeasure period)

noncomputable def EulerLiftedGradientSpace.translation (period : ℝ) [Fact (0 < period)] (a : LiftDomain period) : ↥(LiftL2 period) →ₗᵢ[ℝ] ↥(LiftL2 period)

The measure preserving translation isometry on the actual L² space.

Equations

• EulerLiftedGradientSpace.translation period a = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerLiftedGradientSpace.LiftDomain period) => x + a) ⋯

theorem EulerLiftedGradientSpace.translation_ae (period : ℝ) [Fact (0 < period)] (a : LiftDomain period) (f : ↥(LiftL2 period)) : ↑↑((translation period a) f) =ᵐ[liftMeasure period] fun (x : LiftDomain period) => ↑↑f (x + a)

theorem EulerLiftedGradientSpace.translation_norm (period : ℝ) [Fact (0 < period)] (a : LiftDomain period) (f : ↥(LiftL2 period)) : ‖(translation period a) f‖ = ‖f‖

theorem EulerLiftedGradientSpace.translation_add (period : ℝ) [Fact (0 < period)] (a b : LiftDomain period) (f : ↥(LiftL2 period)) : (translation period a) ((translation period b) f) = (translation period (a + b)) f

@[simp]

theorem EulerLiftedGradientSpace.translation_zero (period : ℝ) [Fact (0 < period)] (f : ↥(LiftL2 period)) : (translation period 0) f = f

noncomputable def EulerLiftedGradientSpace.testGradientLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : ↥(LiftL2 period)

The L² element represented by an actual smooth compact test gradient.

Equations

• EulerLiftedGradientSpace.testGradientLp period κ m φ hφ = MeasureTheory.MemLp.toLp (EulerLiftedGradientSpace.liftedGradient period κ m φ) ⋯

theorem EulerLiftedGradientSpace.testGradientLp_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : ↑↑(testGradientLp period κ m φ hφ) =ᵐ[liftMeasure period] liftedGradient period κ m φ

theorem EulerLiftedGradientSpace.testGradientLp_mem_generators (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : testGradientLp period κ m φ hφ ∈ {g : ↥(LiftL2 period) | ∃ (φ : LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) ∧ ↑↑g =ᵐ[liftMeasure period] liftedGradient period κ m φ}

noncomputable def EulerLiftedGradientSpace.gradientSpace (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : Submodule ℝ ↥(LiftL2 period)

Closure of the span of genuine smooth test gradients in the concrete L² space.

Equations

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

theorem EulerLiftedGradientSpace.gradientSpace_closed (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : IsClosed ↑(gradientSpace period κ m)

instance EulerLiftedGradientSpace.gradientSpace_complete (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : CompleteSpace ↥(gradientSpace period κ m)

noncomputable def EulerLiftedGradientSpace.gradientProjection (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : ↥(LiftL2 period) →L[ℝ] ↥(LiftL2 period)

Orthogonal projection onto the closed lifted gradient subspace.

Equations

• EulerLiftedGradientSpace.gradientProjection period κ m = (EulerLiftedGradientSpace.gradientSpace period κ m).starProjection

theorem EulerLiftedGradientSpace.gradientProjection_norm_le (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : ‖gradientProjection period κ m‖ ≤ 1

The projection bound is independent of the frequency parameter κ.

theorem EulerLiftedGradientSpace.gradientProjection_apply_norm_le (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (f : ↥(LiftL2 period)) : ‖(gradientProjection period κ m) f‖ ≤ ‖f‖

theorem EulerLiftedGradientSpace.testGradient_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) {g : ↥(LiftL2 period)} (hg : g ∈ {g : ↥(LiftL2 period) | ∃ (φ : LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) ∧ ↑↑g =ᵐ[liftMeasure period] liftedGradient period κ m φ}) : g ∈ gradientSpace period κ m

theorem EulerLiftedGradientSpace.gradientGenerators_translated (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (a : LiftDomain period) {g : ↥(LiftL2 period)} (hg : g ∈ {g : ↥(LiftL2 period) | ∃ (φ : LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) ∧ ↑↑g =ᵐ[liftMeasure period] liftedGradient period κ m φ}) : (translation period a) g ∈ {g : ↥(LiftL2 period) | ∃ (φ : LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) ∧ ↑↑g =ᵐ[liftMeasure period] liftedGradient period κ m φ}

theorem EulerLiftedGradientSpace.gradientSpace_translation_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (a : LiftDomain period) {g : ↥(LiftL2 period)} (hg : g ∈ gradientSpace period κ m) : (translation period a) g ∈ gradientSpace period κ m

theorem EulerLiftedGradientSpace.gradientSpace_map_translation (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (a : LiftDomain period) : Submodule.map (translation period a).toLinearMap (gradientSpace period κ m) = gradientSpace period κ m

theorem EulerLiftedGradientSpace.gradientProjection_translation (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) (a : LiftDomain period) (f : ↥(LiftL2 period)) : (translation period a) ((gradientProjection period κ m) f) = (gradientProjection period κ m) ((translation period a) f)

Orthogonal pressure projection commutes with every spatial or angular translation.

noncomputable def EulerLiftedGradientSpace.divergenceFreeSpace (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) : Submodule ℝ ↥(LiftL2 period)

The concrete L² weak divergence-free subspace.

Equations

• EulerLiftedGradientSpace.divergenceFreeSpace period κ m = (EulerLiftedGradientSpace.gradientSpace period κ m)ᗮ

theorem EulerLiftedGradientSpace.pressure_pairing_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) {p e : ↥(LiftL2 period)} (hp : p ∈ gradientSpace period κ m) (he : e ∈ divergenceFreeSpace period κ m) : inner ℝ p e = 0

Pressure cancellation in the concrete lifted L² space.

theorem EulerLiftedGradientSpace.testGradient_pairing_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) {g e : ↥(LiftL2 period)} (hg : g ∈ {g : ↥(LiftL2 period) | ∃ (φ : LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) ∧ ↑↑g =ᵐ[liftMeasure period] liftedGradient period κ m φ}) (he : e ∈ divergenceFreeSpace period κ m) : inner ℝ g e = 0

theorem EulerLiftedGradientSpace.weak_divergence_test_integral (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : Vector3) {e : ↥(LiftL2 period)} (he : e ∈ divergenceFreeSpace period κ m) (φ : LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : LiftDomain period), ContDiff ℝ (↑⊤) (localLift period φ x)) : ∫ (x : LiftDomain period), inner ℝ (liftedGradient period κ m φ x) (↑↑e x) ∂liftMeasure period = 0

Orthogonality is the actual weak-divergence integral against every smooth compact test.