Genuine mixed cutoff Newtonian operators and their quantitative dependence on both cutoffs.

theorem EulerMeanBoundary.Cutoff.ext {χ ψ : Cutoff} (h : χ.field = ψ.field) : χ = ψ

theorem EulerMeanBoundary.Cutoff.ext_iff {χ ψ : Cutoff} : χ = ψ ↔ χ.field = ψ.field

def EulerMeanBoundary.Cutoff.add (χ ψ : Cutoff) : Cutoff

Add, given by ⟨χ.field + ψ.field, χ.smooth.add ψ.smooth, χ.compact.add ψ.compact⟩.

Equations

• χ.add ψ = { field := χ.field + ψ.field, smooth := ⋯, compact := ⋯ }

def EulerMeanBoundary.Cutoff.scale (χ : Cutoff) (c : ℝ) : Cutoff

Scale, given by ⟨c • χ.field, χ.smooth.const_smul c, χ.compact.comp_left (g := fun t : ℝ => c • t) (smul_zero c)⟩.

Equations

• χ.scale c = { field := c • χ.field, smooth := ⋯, compact := ⋯ }

def EulerMeanBoundary.Cutoff.sub (χ ψ : Cutoff) : Cutoff

Sub, given by ⟨χ.field - ψ.field, χ.smooth.sub ψ.smooth, χ.compact.sub ψ.compact⟩.

Equations

• χ.sub ψ = { field := χ.field - ψ.field, smooth := ⋯, compact := ⋯ }

def EulerMeanBoundary.Cutoff.translate (χ : Cutoff) (a : EulerSmoothLimit.Space) : Cutoff

Translate, given by ⟨fun x => χ.field (x+a), χ.smooth.comp (contDiff_id.add contDiff_const), χ.compact.comp_homeomorph (Homeomorph.addRight a)⟩.

Equations

• χ.translate a = { field := fun (x : EulerSmoothLimit.Space) => χ.field (x + a), smooth := ⋯, compact := ⋯ }

noncomputable def EulerMeanBoundary.Cutoff.derivative (χ : Cutoff) (i : Fin 3) : Cutoff

Derivative, given by ⟨partialDerivative χ.field i, contDiff_partialDerivative χ.field χ.smooth i, χ.compact.fderiv_apply ℝ (EuclideanSpace.single i 1)⟩.

Equations

• χ.derivative i = { field := EulerVectorCalculus.partialDerivative χ.field i, smooth := ⋯, compact := ⋯ }

theorem EulerMeanBoundary.testCurl_cutoff_add (χ ψ : Cutoff) (f : EulerMeanGradientTest.Test) : testCurl (χ.add ψ) f = testCurl χ f + testCurl ψ f

theorem EulerMeanBoundary.testCurl_cutoff_scale (χ : Cutoff) (c : ℝ) (f : EulerMeanGradientTest.Test) : testCurl (χ.scale c) f = c • testCurl χ f

theorem EulerMeanBoundary.cutoffCurl_add (χ ψ : Cutoff) : cutoffCurl (χ.add ψ) = cutoffCurl χ + cutoffCurl ψ

theorem EulerMeanBoundary.cutoffCurl_scale (χ : Cutoff) (c : ℝ) : cutoffCurl (χ.scale c) = c • cutoffCurl χ

theorem EulerMeanBoundary.cutoffCurl_sub (χ ψ : Cutoff) : cutoffCurl (χ.sub ψ) = cutoffCurl χ - cutoffCurl ψ

theorem EulerMeanBoundary.weakPotential_add (χ ψ : Cutoff) : weakPotential (χ.add ψ) = weakPotential χ + weakPotential ψ

theorem EulerMeanBoundary.weakPotential_scale (χ : Cutoff) (c : ℝ) : weakPotential (χ.scale c) = c • weakPotential χ

theorem EulerMeanBoundary.weakPotential_sub (χ ψ : Cutoff) : weakPotential (χ.sub ψ) = weakPotential χ - weakPotential ψ

noncomputable def EulerMeanBoundary.mixedBoundaryOperator (χ ψ : Cutoff) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

The literal weak curl χ (-Δ)⁻¹ ψ curl operator.

Equations

• EulerMeanBoundary.mixedBoundaryOperator χ ψ = EulerMeanBoundary.cutoffCurl χ ∘SL EulerMeanBoundary.weakPotential ψ

theorem EulerMeanBoundary.mixedBoundaryOperator_diagonal (χ : Cutoff) : mixedBoundaryOperator χ χ = boundaryOperator χ

theorem EulerMeanBoundary.mixedBoundaryOperator_norm_le (χ ψ : Cutoff) : ‖mixedBoundaryOperator χ ψ‖ ≤ cutoffBound χ * cutoffBound ψ

theorem EulerMeanBoundary.mixedBoundaryOperator_pairing (χ ψ : Cutoff) (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ ((mixedBoundaryOperator χ ψ) u) v = inner ℝ ((weakPotential ψ) u) ((weakPotential χ) v)

theorem EulerMeanBoundary.mixedBoundaryOperator_adjoint (χ ψ : Cutoff) : ContinuousLinearMap.adjoint (mixedBoundaryOperator χ ψ) = mixedBoundaryOperator ψ χ

theorem EulerMeanBoundary.mixedBoundaryOperator_solenoidal (χ ψ : Cutoff) (u : ↥EulerMeanSolenoidal.L2) : (mixedBoundaryOperator χ ψ) u ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerMeanBoundary.mixedBoundaryOperator_supported (χ ψ : Cutoff) (u : ↥EulerMeanSolenoidal.L2) : (mixedBoundaryOperator χ ψ) u ∈ supportedSpace χ

theorem EulerMeanBoundary.mixedBoundaryOperator_add_left (χ ψ ρ : Cutoff) : mixedBoundaryOperator (χ.add ψ) ρ = mixedBoundaryOperator χ ρ + mixedBoundaryOperator ψ ρ

theorem EulerMeanBoundary.mixedBoundaryOperator_add_right (χ ψ ρ : Cutoff) : mixedBoundaryOperator χ (ψ.add ρ) = mixedBoundaryOperator χ ψ + mixedBoundaryOperator χ ρ

theorem EulerMeanBoundary.mixedBoundaryOperator_scale_left (χ ψ : Cutoff) (c : ℝ) : mixedBoundaryOperator (χ.scale c) ψ = c • mixedBoundaryOperator χ ψ

theorem EulerMeanBoundary.mixedBoundaryOperator_scale_right (χ ψ : Cutoff) (c : ℝ) : mixedBoundaryOperator χ (ψ.scale c) = c • mixedBoundaryOperator χ ψ

theorem EulerMeanBoundary.mixedBoundaryOperator_sub_left (χ ψ ρ : Cutoff) : mixedBoundaryOperator (χ.sub ψ) ρ = mixedBoundaryOperator χ ρ - mixedBoundaryOperator ψ ρ

theorem EulerMeanBoundary.mixedBoundaryOperator_sub_right (χ ψ ρ : Cutoff) : mixedBoundaryOperator χ (ψ.sub ρ) = mixedBoundaryOperator χ ψ - mixedBoundaryOperator χ ρ

theorem EulerMeanBoundary.mixedBoundaryOperator_difference (χ₁ χ₀ ψ₁ ψ₀ : Cutoff) : mixedBoundaryOperator χ₁ ψ₁ - mixedBoundaryOperator χ₀ ψ₀ = mixedBoundaryOperator (χ₁.sub χ₀) ψ₁ + mixedBoundaryOperator χ₀ (ψ₁.sub ψ₀)

The two actual coefficient differences are split between the two cutoff positions.

theorem EulerMeanBoundary.mixedBoundaryOperator_difference_norm_le (χ₁ χ₀ ψ₁ ψ₀ : Cutoff) : ‖mixedBoundaryOperator χ₁ ψ₁ - mixedBoundaryOperator χ₀ ψ₀‖ ≤ cutoffBound (χ₁.sub χ₀) * cutoffBound ψ₁ + cutoffBound χ₀ * cutoffBound (ψ₁.sub ψ₀)