Elliptic recovery for classical fields without assuming Sobolev regularity.

The localized identities below require only ordinary smoothness and a compactly supported scalar cutoff. In particular, they do not assume that derivatives of the velocity are globally square integrable.

theorem EulerComparatorRecovery.integrable_and_integral_le_of_nonnegative_limit {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (F : ℕ → X → ℝ) (f : X → ℝ) (C : ℝ) (hF : ∀ (n : ℕ), MeasureTheory.Integrable (F n) μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hF0 : ∀ (n : ℕ) (x : X), 0 ≤ F n x) (hf0 : ∀ (x : X), 0 ≤ f x) (hlim : ∀ (x : X), Filter.Tendsto (fun (n : ℕ) => F n x) Filter.atTop (nhds (f x))) (hbound : ∀ (n : ℕ), ∫ (x : X), F n x ∂μ ≤ C) : MeasureTheory.Integrable f μ ∧ ∫ (x : X), f x ∂μ ≤ C

Fatou's lemma turns uniform integral bounds on nonnegative localizations into integrability of the pointwise limit.

theorem EulerComparatorRecovery.localized_dirichlet_identity (η h : EulerSmoothLimit.Space → ℝ) (hcη : HasCompactSupport η) (hη : ContDiff ℝ (↑⊤) η) (hh : ContDiff ℝ (↑⊤) h) : ∫ (x : EulerSmoothLimit.Space), ‖gradient (η * h) x‖ ^ 2 = (∫ (x : EulerSmoothLimit.Space), h x ^ 2 * ‖gradient η x‖ ^ 2) - ∫ (x : EulerSmoothLimit.Space), η x ^ 2 * (h x * Laplacian.laplacian h x)

The source term retained in the localized Dirichlet identity.

theorem EulerComparatorRecovery.scalar_laplacian_smooth (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) : ContDiff ℝ (↑⊤) (Laplacian.laplacian h)

Smoothness of the scalar Laplacian follows directly from coordinate derivatives, with no global integrability premise.

theorem EulerComparatorRecovery.gradient_energy_recovery (M : ℝ) (hgrad : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖gradient (EulerLpTranslation.cutoff n) x‖ ≤ M) (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hL2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hcΔ : HasCompactSupport (Laplacian.laplacian h)) : MeasureTheory.MemLp (gradient h) 2 MeasureTheory.volume ∧ ∫ (x : EulerSmoothLimit.Space), ‖gradient h x‖ ^ 2 ≤ (M ^ 2 * ∫ (x : EulerSmoothLimit.Space), h x ^ 2) + ∫ (x : EulerSmoothLimit.Space), |h x * Laplacian.laplacian h x|

A smooth square-integrable function whose Laplacian has compact support has square-integrable first derivatives. The proof first localizes and only then invokes Fatou; no derivative integrability is assumed.

theorem EulerComparatorRecovery.exists_gradient_energy_bound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (h : EulerSmoothLimit.Space → ℝ), ContDiff ℝ (↑⊤) h → MeasureTheory.MemLp h 2 MeasureTheory.volume → HasCompactSupport (Laplacian.laplacian h) → MeasureTheory.MemLp (gradient h) 2 MeasureTheory.volume ∧ ∫ (x : EulerSmoothLimit.Space), ‖gradient h x‖ ^ 2 ≤ (M ^ 2 * ∫ (x : EulerSmoothLimit.Space), h x ^ 2) + ∫ (x : EulerSmoothLimit.Space), |h x * Laplacian.laplacian h x|

A single fixed cutoff constant works for every scalar field.

theorem EulerComparatorRecovery.gradient_memLp_of_laplacian_compact (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hL2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hcΔ : HasCompactSupport (Laplacian.laplacian h)) : MeasureTheory.MemLp (gradient h) 2 MeasureTheory.volume

theorem EulerComparatorRecovery.exists_gradient_energy_square_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h : EulerSmoothLimit.Space → ℝ), ContDiff ℝ (↑⊤) h → MeasureTheory.MemLp h 2 MeasureTheory.volume → HasCompactSupport (Laplacian.laplacian h) → ∫ (x : EulerSmoothLimit.Space), ‖gradient h x‖ ^ 2 ≤ (C * ∫ (x : EulerSmoothLimit.Space), h x ^ 2) + ∫ (x : EulerSmoothLimit.Space), Laplacian.laplacian h x ^ 2

A convenient quadratic estimate for uniform-in-time bootstrapping: the constant is independent of the field and of the support of its Laplacian.

theorem EulerComparatorRecovery.laplacian_compact_of_curl_compact (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (hc : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl u)) : HasCompactSupport (Laplacian.laplacian u)

Compact vorticity forces the Laplacian to be compactly supported. No integrability hypothesis on derivatives of the velocity is used here.

theorem EulerComparatorRecovery.laplacian_wordDerivative (word : List (Fin 3)) (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) : Laplacian.laplacian (EulerMeanHarmonic.wordDerivative word h) = EulerMeanHarmonic.wordDerivative word (Laplacian.laplacian h)

The Laplacian commutes with every finite coordinate derivative word.

theorem EulerComparatorRecovery.wordDerivative_compact (word : List (Fin 3)) (h : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport h) : HasCompactSupport (EulerMeanHarmonic.wordDerivative word h)

theorem EulerComparatorRecovery.wordDerivative_memLp_of_laplacian_compact (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hL2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hcΔ : HasCompactSupport (Laplacian.laplacian h)) (word : List (Fin 3)) : MeasureTheory.MemLp (EulerMeanHarmonic.wordDerivative word h) 2 MeasureTheory.volume

Every coordinate derivative of a smooth L² scalar with compact Laplacian is L², proved inductively from the noncircular first-derivative estimate.

def EulerComparatorRecovery.wordEnergyBound (C : ℝ) (h : EulerSmoothLimit.Space → ℝ) : List (Fin 3) → ℝ

Recursive bounds separate the original finite energy from compactly supported derivatives of the Laplacian.

Equations

• One or more equations did not get rendered due to their size.
• EulerComparatorRecovery.wordEnergyBound C h [] = ∫ (x : EulerSmoothLimit.Space), h x ^ 2

theorem EulerComparatorRecovery.wordDerivative_energy_le (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ (f : EulerSmoothLimit.Space → ℝ), ContDiff ℝ (↑⊤) f → MeasureTheory.MemLp f 2 MeasureTheory.volume → HasCompactSupport (Laplacian.laplacian f) → ∫ (x : EulerSmoothLimit.Space), ‖gradient f x‖ ^ 2 ≤ (C * ∫ (x : EulerSmoothLimit.Space), f x ^ 2) + ∫ (x : EulerSmoothLimit.Space), Laplacian.laplacian f x ^ 2) (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hL2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hcΔ : HasCompactSupport (Laplacian.laplacian h)) (word : List (Fin 3)) : ∫ (x : EulerSmoothLimit.Space), EulerMeanHarmonic.wordDerivative word h x ^ 2 ≤ wordEnergyBound C h word

theorem EulerComparatorRecovery.wordDerivative_energy_uniform {ι : Type u_1} (h : ι → EulerSmoothLimit.Space → ℝ) (hs : ∀ (t : ι), ContDiff ℝ (↑⊤) (h t)) (hL2 : ∀ (t : ι), MeasureTheory.MemLp (h t) 2 MeasureTheory.volume) (hcΔ : ∀ (t : ι), HasCompactSupport (Laplacian.laplacian (h t))) (h0 : ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), h t x ^ 2 ≤ B) (hsource : ∀ (word : List (Fin 3)), ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), EulerMeanHarmonic.wordDerivative word (Laplacian.laplacian (h t)) x ^ 2 ≤ B) (word : List (Fin 3)) : ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), EulerMeanHarmonic.wordDerivative word (h t) x ^ 2 ≤ B

Uniform finite energy and uniform energies of the compact Laplacian jets give uniform energies of every velocity jet. The parameter set is arbitrary, so this applies directly to a compact time interval.

theorem EulerComparatorRecovery.component_wordDerivative_memLp (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hL2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (hc : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl u)) (j : Fin 3) (word : List (Fin 3)) : MeasureTheory.MemLp (EulerMeanHarmonic.wordDerivative word fun (x : EulerSmoothLimit.Space) => (u x).ofLp j) 2 MeasureTheory.volume

Every scalar coordinate derivative of a divergence-free smooth finite energy velocity with compact vorticity is square integrable.

theorem EulerComparatorRecovery.component_wordDerivative_energy_uniform {ι : Type u_1} (u : ι → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ι), ContDiff ℝ (↑⊤) (u t)) (hL2 : ∀ (t : ι), MeasureTheory.MemLp (u t) 2 MeasureTheory.volume) (hdiv : ∀ (t : ι) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (u t) x = 0) (hc : ∀ (t : ι), HasCompactSupport (EulerMeanCutoffCurl.vectorCurl (u t))) (h0 : ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), ‖u t x‖ ^ 2 ≤ B) (hsource : ∀ (j : Fin 3) (word : List (Fin 3)), ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), EulerMeanHarmonic.wordDerivative word (fun (y : EulerSmoothLimit.Space) => (Laplacian.laplacian (u t) y).ofLp j) x ^ 2 ≤ B) (j : Fin 3) (word : List (Fin 3)) : ∃ (B : ℝ), ∀ (t : ι), ∫ (x : EulerSmoothLimit.Space), EulerMeanHarmonic.wordDerivative word (fun (y : EulerSmoothLimit.Space) => (u t y).ofLp j) x ^ 2 ≤ B

Uniform velocity energy and uniform compact Laplacian-jet energies give uniform bounds for every scalar coordinate jet of a divergence-free velocity.