Sobolev Products

theorem EulerSobolevProducts.sobolevNorm_zero (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolev.sobolevNorm d 0 f = ‖f.toLp 2 MeasureTheory.volume‖

theorem EulerSobolevProducts.besselWeight_mono (d : ℕ) {s t : ℝ} (hst : s ≤ t) (ξ : EulerSobolev.Domain d) : EulerSobolev.besselWeight d s ξ ≤ EulerSobolev.besselWeight d t ξ

theorem EulerSobolevProducts.sobolevNorm_mono (d : ℕ) {s t : ℝ} (hst : s ≤ t) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolev.sobolevNorm d s f ≤ EulerSobolev.sobolevNorm d t f

theorem EulerSobolevProducts.directional_eq_iteratedDeriv (d n : ℕ) (v x : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : (directional d n v f) x = iteratedDeriv n (fun (t : ℝ) => f (x + t • v)) 0

noncomputable def EulerSobolevProducts.product (d : ℕ) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : SchwartzMap (EulerSobolev.Domain d) ℂ

Pointwise multiplication of two complex Schwartz functions.

Equations

• EulerSobolevProducts.product d f g = ((SchwartzMap.pairing (ContinuousLinearMap.mul ℂ ℂ)) f) g

@[simp]

theorem EulerSobolevProducts.product_apply (d : ℕ) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) (x : EulerSobolev.Domain d) : (product d f g) x = f x * g x

theorem EulerSobolevProducts.directional_product (d n : ℕ) (v : EulerSobolev.Domain d) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : directional d n v (product d f g) = ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) • product d (directional d j v f) (directional d (n - j) v g)

theorem EulerSobolevProducts.directional_L2_le (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(directional d n v f).toLp 2 MeasureTheory.volume‖ ≤ (2 * Real.pi) ^ n * ‖v‖ ^ n * EulerSobolev.sobolevNorm d (↑n) f

theorem EulerSobolevProducts.besselWeight_six_le_pure_six (d : ℕ) (ξ : EulerSobolev.Domain d) : EulerSobolev.besselWeight d 6 ξ ≤ (↑d + 1) ^ 2 * (1 + ∑ i : Fin d, ‖ξ.ofLp i‖ ^ 6)

theorem EulerSobolevProducts.fourier_directional_norm (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) (ξ : EulerSobolev.Domain d) : ‖(EulerSobolev.schwartzFourier (directional d n v f)) ξ‖ = (2 * Real.pi) ^ n * ‖inner ℝ ξ v‖ ^ n * ‖(EulerSobolev.schwartzFourier f) ξ‖

noncomputable def EulerSobolevProducts.normLp (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The pointwise norm of a Schwartz function, represented in the real L² space.

Equations

• EulerSobolevProducts.normLp d f = MeasureTheory.MemLp.toLp (fun (x : EulerSobolev.Domain d) => ‖f x‖) ⋯

theorem EulerSobolevProducts.norm_normLp (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖normLp d f‖ = ‖f.toLp 2 MeasureTheory.volume‖

theorem EulerSobolevProducts.coe_normLp (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ↑↑(normLp d f) =ᵐ[MeasureTheory.volume] fun (x : EulerSobolev.Domain d) => ‖f x‖

theorem EulerSobolevProducts.normLp_le_sum {ι : Type u_1} [Fintype ι] (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) (g : ι → SchwartzMap (EulerSobolev.Domain d) ℂ) (C : ℝ) (hC : 0 ≤ C) (h : ∀ (x : EulerSobolev.Domain d), ‖f x‖ ≤ C * ∑ i : ι, ‖(g i) x‖) : ‖f.toLp 2 MeasureTheory.volume‖ ≤ C * ∑ i : ι, ‖(g i).toLp 2 MeasureTheory.volume‖

theorem EulerSobolevProducts.sobolevNorm_six_le_pure_derivatives (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolev.sobolevNorm d 6 f ≤ (↑d + 1) ^ 2 * (‖f.toLp 2 MeasureTheory.volume‖ + (2 * Real.pi) ^ (-6) * ∑ i : Fin d, ‖(directional d 6 (EuclideanSpace.single i 1) f).toLp 2 MeasureTheory.volume‖)

theorem EulerSobolevProducts.product_L2_le_of_sup (d : ℕ) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) (A : ℝ) (hA : ∀ (x : EulerSobolev.Domain d), ‖f x‖ ≤ A) : ‖(product d f g).toLp 2 MeasureTheory.volume‖ ≤ A * ‖g.toLp 2 MeasureTheory.volume‖

theorem EulerSobolevProducts.directional_sup_le_H6 (d j : ℕ) (hd : ↑d < 2 * 3) (hj : j ≤ 3) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) (x : EulerSobolev.Domain d) : ‖(directional d j v f) x‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ j * EulerSobolev.sobolevNorm d 6 f

theorem EulerSobolevProducts.directional_L2_le_H6 (d j : ℕ) (hj : j ≤ 6) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(directional d j v f).toLp 2 MeasureTheory.volume‖ ≤ (2 * Real.pi) ^ j * EulerSobolev.sobolevNorm d 6 f

theorem EulerSobolevProducts.product_directional_L2_le_left (d j k : ℕ) (hd : ↑d < 2 * 3) (hj : j ≤ 3) (hk : k ≤ 6) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(product d (directional d j v f) (directional d k v g)).toLp 2 MeasureTheory.volume‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ (j + k) * EulerSobolev.sobolevNorm d 6 f * EulerSobolev.sobolevNorm d 6 g

theorem EulerSobolevProducts.product_directional_L2_le (d j k : ℕ) (hd : ↑d < 2 * 3) (hjk : j + k ≤ 6) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(product d (directional d j v f) (directional d k v g)).toLp 2 MeasureTheory.volume‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ (j + k) * EulerSobolev.sobolevNorm d 6 f * EulerSobolev.sobolevNorm d 6 g

theorem EulerSobolevProducts.directional_product_L2_le (d n : ℕ) (hd : ↑d < 2 * 3) (hn : n ≤ 6) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(directional d n v (product d f g)).toLp 2 MeasureTheory.volume‖ ≤ 2 ^ n * (EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ n * EulerSobolev.sobolevNorm d 6 f * EulerSobolev.sobolevNorm d 6 g)

theorem EulerSobolevProducts.sobolevNorm_six_product (d : ℕ) (hd : ↑d < 2 * 3) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolev.sobolevNorm d 6 (product d f g) ≤ (↑d + 1) ^ 2 * (1 + 64 * ↑d) * EulerSobolev.embeddingConstant d 3 hd * EulerSobolev.sobolevNorm d 6 f * EulerSobolev.sobolevNorm d 6 g

A concrete algebra constant, obtained by Leibniz, Plancherel and the Sobolev embedding.

theorem EulerSobolevProducts.four_dimensional_H6_algebra (f g : SchwartzMap (EulerSobolev.Domain 4) ℂ) : EulerSobolev.sobolevNorm 4 6 (product 4 f g) ≤ 6425 * EulerSobolev.embeddingConstant 4 3 four_dimensional_H6_algebra._proof_1 * EulerSobolev.sobolevNorm 4 6 f * EulerSobolev.sobolevNorm 4 6 g

The fixed four-dimensional H⁶ algebra estimate used in the packet energy argument.

The fixed-order transport commutator estimate.

theorem EulerSobolevTransport.directional_sup_le_H5 (d j : ℕ) (hd : ↑d < 2 * 3) (hj : j ≤ 2) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) (x : EulerSobolev.Domain d) : ‖(EulerSobolevProducts.directional d j v f) x‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ j * EulerSobolev.sobolevNorm d 5 f

theorem EulerSobolevTransport.directional_L2_le_H5 (d j : ℕ) (hj : j ≤ 5) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(EulerSobolevProducts.directional d j v f).toLp 2 MeasureTheory.volume‖ ≤ (2 * Real.pi) ^ j * EulerSobolev.sobolevNorm d 5 f

theorem EulerSobolevTransport.product_directional_L2_H5_left (d j k : ℕ) (hd : ↑d < 2 * 3) (hj : j ≤ 2) (hk : k ≤ 5) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(EulerSobolevProducts.product d (EulerSobolevProducts.directional d j v f) (EulerSobolevProducts.directional d k v g)).toLp 2 MeasureTheory.volume‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ (j + k) * EulerSobolev.sobolevNorm d 5 f * EulerSobolev.sobolevNorm d 5 g

theorem EulerSobolevTransport.product_directional_L2_H5 (d j k : ℕ) (hd : ↑d < 2 * 3) (hjk : j + k ≤ 5) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (f g : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(EulerSobolevProducts.product d (EulerSobolevProducts.directional d j v f) (EulerSobolevProducts.directional d k v g)).toLp 2 MeasureTheory.volume‖ ≤ EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ (j + k) * EulerSobolev.sobolevNorm d 5 f * EulerSobolev.sobolevNorm d 5 g

noncomputable def EulerSobolevTransport.commutator (d n : ℕ) (v : EulerSobolev.Domain d) (b h : SchwartzMap (EulerSobolev.Domain d) ℂ) : SchwartzMap (EulerSobolev.Domain d) ℂ

The actual commutator of an iterated directional derivative with multiplication.

Equations

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

theorem EulerSobolevTransport.directional_succ_right (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolevProducts.directional d (n + 1) v f = EulerSobolevProducts.directional d n v (EulerSobolevProducts.directional d 1 v f)

theorem EulerSobolevTransport.commutator_expansion (d n : ℕ) (v : EulerSobolev.Domain d) (b h : SchwartzMap (EulerSobolev.Domain d) ℂ) : commutator d n v b h = ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) • EulerSobolevProducts.product d (EulerSobolevProducts.directional d j v (EulerSobolevProducts.directional d 1 v b)) (EulerSobolevProducts.directional d (n - (j + 1)) v h)

theorem EulerSobolevTransport.sum_choose_successors_le (n : ℕ) : ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) ≤ 2 ^ n

theorem EulerSobolevTransport.transport_commutator_L2 (d n : ℕ) (hd : ↑d < 2 * 3) (hn : n ≤ 6) (v : EulerSobolev.Domain d) (hv : ‖v‖ ≤ 1) (b h : SchwartzMap (EulerSobolev.Domain d) ℂ) : ‖(commutator d n v b h).toLp 2 MeasureTheory.volume‖ ≤ 2 ^ n * (EulerSobolev.embeddingConstant d 3 hd * (2 * Real.pi) ^ (n - 1) * EulerSobolev.sobolevNorm d 5 (EulerSobolevProducts.directional d 1 v b) * EulerSobolev.sobolevNorm d 5 h)

No derivative is lost in the fixed-order transport commutator: after removing the top term, one derivative falls on b, leaving a total of at most five.