The actual homogeneous first-order test space on ordinary Euclidean three-space.

def EulerMeanGradientTest.testSpace : Submodule ℝ (EulerSmoothLimit.Space → EulerSmoothLimit.Space)

Smooth compactly supported vector fields, as a genuine function submodule.

Equations

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

@[reducible, inline]

abbrev EulerMeanGradientTest.Test : Type

Test: an abbreviation for ↥testSpace.

Equations

• EulerMeanGradientTest.Test = ↥EulerMeanGradientTest.testSpace

theorem EulerMeanGradientTest.Test.smooth (f : Test) : ContDiff ℝ ↑⊤ ↑f

theorem EulerMeanGradientTest.Test.compact (f : Test) : HasCompactSupport ↑f

theorem EulerMeanGradientTest.Test.column_memLp (f : Test) (i : Fin 3) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (↑f) x) (EuclideanSpace.single i 1)) 2 MeasureTheory.volume

noncomputable def EulerMeanGradientTest.derivativeColumn (f : Test) (i : Fin 3) : ↥EulerMeanSolenoidal.L2

A genuine distributional/classical derivative column as an L² vector field.

Equations

• EulerMeanGradientTest.derivativeColumn f i = MeasureTheory.MemLp.toLp (fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (↑f) x) (EuclideanSpace.single i 1)) ⋯

theorem EulerMeanGradientTest.derivativeColumn_ae (f : Test) (i : Fin 3) : ↑↑(derivativeColumn f i) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (↑f) x) (EuclideanSpace.single i 1)

theorem EulerMeanGradientTest.derivativeColumn_add (f g : Test) (i : Fin 3) : derivativeColumn (f + g) i = derivativeColumn f i + derivativeColumn g i

theorem EulerMeanGradientTest.derivativeColumn_smul (c : ℝ) (f : Test) (i : Fin 3) : derivativeColumn (c • f) i = c • derivativeColumn f i

@[reducible, inline]

abbrev EulerMeanGradientTest.GradientTensor : Type

The Hilbert space of three L² derivative columns, with the Frobenius norm.

Equations

• EulerMeanGradientTest.GradientTensor = PiLp 2 fun (x : Fin 3) => ↥EulerMeanSolenoidal.L2

noncomputable def EulerMeanGradientTest.testGradient : Test →ₗ[ℝ] GradientTensor

The actual gradient map on compact smooth vector tests.

Equations

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

theorem EulerMeanGradientTest.testGradient_apply (f : Test) (i : Fin 3) : (testGradient f).ofLp i = derivativeColumn f i

theorem EulerMeanGradientTest.opNorm_le_sum_columns (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ‖A‖ ≤ ∑ i : Fin 3, ‖A (EuclideanSpace.single i 1)‖

The operator norm is bounded by the sum of the Euclidean derivative-column norms.

theorem EulerMeanGradientTest.lpNorm_fderiv_le_gradient (f : Test) : MeasureTheory.lpNorm (fderiv ℝ ↑f) 2 MeasureTheory.volume ≤ 3 * ‖testGradient f‖

The derivative norm used by the cutoff bound is controlled by the actual Hilbert gradient norm.

noncomputable def EulerMeanGradientTest.homogeneousSpace : Submodule ℝ GradientTensor

Homogeneous H¹ is the closed subspace generated by actual compact test gradients.

Equations

• EulerMeanGradientTest.homogeneousSpace = EulerMeanGradientTest.testGradient.range.topologicalClosure

instance EulerMeanGradientTest.instCompleteSpaceSubtypeGradientTensorMemSubmoduleRealHomogeneousSpace : CompleteSpace ↥homogeneousSpace

noncomputable def EulerMeanGradientTest.homogeneousGradient : Test →ₗ[ℝ] ↥homogeneousSpace

The dense map from genuine tests into the homogeneous Hilbert space.

Equations

• EulerMeanGradientTest.homogeneousGradient = LinearMap.codRestrict EulerMeanGradientTest.homogeneousSpace EulerMeanGradientTest.testGradient EulerMeanGradientTest.homogeneousGradient._proof_1

theorem EulerMeanGradientTest.homogeneousGradient_dense : DenseRange ⇑homogeneousGradient