Sobolev Inequalities

Generic inequalities for sobolevNormSqDistrib and MemSobolevDistrib. These are tools applicable across the NashEmbedding.Sobolev infrastructure, not specific to any particular construction (mollifier, Riemann sum, etc.).

theorem NashEmbedding.Sobolev.sobolevNormSqDistrib_triangle {n : ℕ} (s : ℝ) (a b c : TrigPolyDual n) (hab : MemSobolevDistrib n s (a - b)) (hbc : MemSobolevDistrib n s (b - c)) : sobolevNormSqDistrib n s (a - c) ≤ 2 * sobolevNormSqDistrib n s (a - b) + 2 * sobolevNormSqDistrib n s (b - c)

Closure properties of MemSobolevDistrib and integrationEmbed

theorem NashEmbedding.Sobolev.MemSobolevDistrib.sub {n : ℕ} {s : ℝ} {a b : TrigPolyDual n} (ha : MemSobolevDistrib n s a) (hb : MemSobolevDistrib n s b) : MemSobolevDistrib n s (a - b)

integrationEmbed linearity (subject to continuity)

The unconditional identities ι(f + g) = ι(f) + ι(g) and ι(f - g) = ι(f) - ι(g) are FALSE: Bochner-integral additivity fails when one of the two functions is non-integrable on the period cube [0, 2π]ⁿ. The identities do hold once integrability of the integrands f · e_{-m} and g · e_{-m} on the period cube is available. We package this as a continuity hypothesis on f and g: continuous ⟹ (continuous × continuous bounded) ⟹ integrable on the compact period cube, and additivity of the Bochner integral kicks in.

Consumers that only have IntegrableOn f (weaker than Continuous f) would need a variant with IntegrableOn hypotheses and a MeasureTheory.Integrable.bdd_mul-style step to get integrability of f · e_{-m}; not needed here.

theorem NashEmbedding.Sobolev.integrationEmbed_add {n : ℕ} {f g : (Fin n → ℝ) → ℂ} (hf : Continuous f) (hg : Continuous g) : (integrationEmbed n fun (x : Fin n → ℝ) => f x + g x) = integrationEmbed n f + integrationEmbed n g

integrationEmbed is additive on continuous functions: ι(f + g) = ι(f) + ι(g). Continuity is needed to give Bochner-integral additivity of the integrands f · e_{-m} and g · e_{-m} on the compact period cube [0, 2π]ⁿ. Without integrability the unconditional identity is false — see the section header.

theorem NashEmbedding.Sobolev.integrationEmbed_sub {n : ℕ} {f g : (Fin n → ℝ) → ℂ} (hf : Continuous f) (hg : Continuous g) : (integrationEmbed n fun (x : Fin n → ℝ) => f x - g x) = integrationEmbed n f - integrationEmbed n g

integrationEmbed distributes over subtraction on continuous functions: ι(f - g) = ι(f) - ι(g). Companion of integrationEmbed_add; same caveat.