noncomputable def TemperedDistributions.japaneseBracket {E : Type u_4} [NormedAddCommGroup E] (x : E) : ℝ

The Japanese bracket ⟨x⟩ = √(1 + ‖x‖²) on a normed space, a smooth weight comparable to 1 + ‖x‖.

theorem TemperedDistributions.japaneseBracket_nonneg {E : Type u_4} [NormedAddCommGroup E] (x : E) : 0 ≤ japaneseBracket x

The Japanese bracket is nonnegative: 0 ≤ ⟨x⟩.

theorem TemperedDistributions.japaneseBracket_le_one_add_norm {E : Type u_4} [NormedAddCommGroup E] (x : E) : japaneseBracket x ≤ 1 + ‖x‖

The Japanese bracket is bounded above by 1 + ‖x‖: ⟨x⟩ ≤ 1 + ‖x‖.

theorem TemperedDistributions.one_add_norm_le_sqrt_two_mul_japaneseBracket {E : Type u_4} [NormedAddCommGroup E] (x : E) : 1 + ‖x‖ ≤ √2 * japaneseBracket x

Reverse comparison: 1 + ‖x‖ ≤ √2 · ⟨x⟩.

theorem TemperedDistributions.japaneseBracket_pow_le_one_add_norm_pow {E : Type u_4} [NormedAddCommGroup E] (x : E) (k : ℕ) : japaneseBracket x ^ k ≤ (1 + ‖x‖) ^ k

Monotone power version: ⟨x⟩^k ≤ (1 + ‖x‖)^k.

theorem TemperedDistributions.one_add_norm_pow_le_sqrt_two_pow_mul_japaneseBracket_pow {E : Type u_4} [NormedAddCommGroup E] (x : E) (k : ℕ) : (1 + ‖x‖) ^ k ≤ √2 ^ k * japaneseBracket x ^ k

Reverse power comparison: (1 + ‖x‖)^k ≤ (√2)^k · ⟨x⟩^k.

theorem TemperedDistributions.weighted_norm_le_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K k n : ℕ} (hk : k ≤ K) (hn : n ≤ K) (f : SchwartzMap E F) (x : E) : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Each weighted derivative norm (1 + ‖x‖)^k · ‖∂^n f(x)‖ is bounded by 2^K times the supremum of Schwartz seminorms of order at most K.

theorem TemperedDistributions.monomial_norm_le_weighted_norm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

The monomial weighted norm ‖x‖^k · ‖∂^n f(x)‖ is bounded by the weighted norm (1 + ‖x‖)^k · ‖∂^n f(x)‖.

noncomputable def TemperedDistributions.weightedCkNorm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K n : ℕ) (f : SchwartzMap E F) : ℝ

The weighted C^k norm of a Schwartz function: the infimum of constants c ≥ 0 bounding (1 + ‖x‖)^K · ‖∂^n f(x)‖ uniformly in x.

theorem TemperedDistributions.weightedCkNorm_bounds_nonempty {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K n : ℕ) (f : SchwartzMap E F) : {c : ℝ | 0 ≤ c ∧ ∀ (x : E), (1 + ‖x‖) ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}.Nonempty

The set of bounds defining weightedCkNorm K n f is nonempty, using Schwartz decay.

theorem TemperedDistributions.weightedCkNorm_bounds_bddBelow {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K n : ℕ) (f : SchwartzMap E F) : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : E), (1 + ‖x‖) ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

The set of bounds defining weightedCkNorm K n f is bounded below by 0.

theorem TemperedDistributions.weightedCkNorm_nonneg {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K n : ℕ) (f : SchwartzMap E F) : 0 ≤ weightedCkNorm K n f

weightedCkNorm K n f is nonnegative.

theorem TemperedDistributions.le_weightedCkNorm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K n : ℕ) (f : SchwartzMap E F) (x : E) : (1 + ‖x‖) ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ weightedCkNorm K n f

Pointwise bound: each value (1 + ‖x‖)^K · ‖∂^n f(x)‖ is dominated by weightedCkNorm K n f.

theorem TemperedDistributions.weightedCkNorm_le_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K n : ℕ} (hn : n ≤ K) (f : SchwartzMap E F) : weightedCkNorm K n f ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

weightedCkNorm K n f ≤ 2^K · sup_{m ≤ (K,K)} seminorm_m f.

theorem TemperedDistributions.seminorm_le_weightedCkNorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K k n : ℕ} (hk : k ≤ K) (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 k n) f ≤ weightedCkNorm K n f

Reverse comparison: any Schwartz seminorm of order (k, n) with k ≤ K is bounded by weightedCkNorm K n f.

noncomputable def TemperedDistributions.weightedCkNormSup {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ℕ) (f : SchwartzMap E F) : ℝ

The maximum of weightedCkNorm K n f over derivative orders n ≤ K.

theorem TemperedDistributions.weightedCkNorm_le_weightedCkNormSup {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ℕ) {n : ℕ} (hn : n ≤ K) (f : SchwartzMap E F) : weightedCkNorm K n f ≤ weightedCkNormSup K f

Individual weightedCkNorm K n f is bounded by the supremum weightedCkNormSup K f when n ≤ K.

theorem TemperedDistributions.seminorm_le_weightedCkNormSup {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K k n : ℕ} (hk : k ≤ K) (hn : n ≤ K) (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 k n) f ≤ weightedCkNormSup K f

Schwartz seminorms with k, n ≤ K are bounded by weightedCkNormSup K f.

theorem TemperedDistributions.weightedCkNormSup_le_sup_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : weightedCkNormSup K f ≤ 2 ^ K * ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f

weightedCkNormSup K f ≤ 2^K · sup_{m ≤ (K,K)} seminorm_m f.

noncomputable def TemperedDistributions.monomialDerivNormSum {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : ℝ

The sum of all Schwartz seminorms of order at most (K, K) applied to f.

theorem TemperedDistributions.monomialDerivNormSum_nonneg {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : 0 ≤ monomialDerivNormSum K f

monomialDerivNormSum K f is nonnegative.

theorem TemperedDistributions.sup_seminorm_le_monomialDerivNormSum {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) f ≤ monomialDerivNormSum K f

The supremum of Schwartz seminorms over Iic (K, K) is bounded by their sum.

theorem TemperedDistributions.card_Iic_pair (K : ℕ) : (Finset.Iic (K, K)).card = (K + 1) ^ 2

Cardinality of Iic (K, K) in ℕ × ℕ equals (K + 1)^2.

theorem TemperedDistributions.weightedCkNormSup_le_two_pow_mul_monomialDerivNormSum {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : weightedCkNormSup K f ≤ 2 ^ K * monomialDerivNormSum K f

weightedCkNormSup K f ≤ 2^K · monomialDerivNormSum K f.

theorem TemperedDistributions.monomialDerivNormSum_le_sq_mul_weightedCkNormSup {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (K : ℕ) (f : SchwartzMap E F) : monomialDerivNormSum K f ≤ ↑((K + 1) ^ 2) * weightedCkNormSup K f

Reverse comparison: monomialDerivNormSum K f ≤ (K + 1)^2 · weightedCkNormSup K f.

def MultiIndexBridge.multiIndexOrder {m : ℕ} (α : Fin m → ℕ) : ℕ

The order |α| = ∑ αᵢ of a multi-index α : Fin m → ℕ.

def MultiIndexBridge.tupleToMultiIndex {m n : ℕ} (σ : Fin n → Fin m) : Fin m → ℕ

From a tuple σ : Fin n → Fin m build the multi-index counting fibers of σ.

theorem MultiIndexBridge.multiIndexOrder_tupleToMultiIndex {m n : ℕ} (σ : Fin n → Fin m) : multiIndexOrder (tupleToMultiIndex σ) = n

The total order of tupleToMultiIndex σ equals n, the length of the tuple.

noncomputable def MultiIndexBridge.multiIndexDirections {m : ℕ} (β : Fin m → ℕ) : Fin (multiIndexOrder β) → EuclideanSpace ℝ (Fin m)

Canonical tuple of unit direction vectors corresponding to a multi-index β, indexed by Fin |β|.

theorem MultiIndexBridge.multiIndexDirections_eq_single {m : ℕ} (β : Fin m → ℕ) (k : Fin (multiIndexOrder β)) : ∃ (i : Fin m), multiIndexDirections β k = EuclideanSpace.single i 1

Each entry of multiIndexDirections β is a standard basis vector.

theorem MultiIndexBridge.norm_multiIndexDirections_le {m : ℕ} (β : Fin m → ℕ) (k : Fin (multiIndexOrder β)) : ‖multiIndexDirections β k‖ ≤ 1

Each direction vector in multiIndexDirections β has norm at most one.

def MultiIndexBridge.realMonomial {m : ℕ} (α : Fin m → ℕ) (x : EuclideanSpace ℝ (Fin m)) : ℝ

The real monomial x^α = ∏ᵢ (xᵢ)^(αᵢ) associated to a multi-index α.

theorem MultiIndexBridge.abs_realMonomial_le_norm_pow {m : ℕ} (α : Fin m → ℕ) (x : EuclideanSpace ℝ (Fin m)) : |realMonomial α x| ≤ ‖x‖ ^ multiIndexOrder α

|x^α| ≤ ‖x‖^{|α|} for any multi-index α.

noncomputable def MultiIndexBridge.multiIndexPartialDeriv {m : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (β : Fin m → ℕ) (f : EuclideanSpace ℝ (Fin m) → F) (x : EuclideanSpace ℝ (Fin m)) : F

The mixed partial derivative ∂^β f(x) of order β, expressed via the iterated Fréchet derivative applied to the canonical direction tuple.

theorem MultiIndexBridge.norm_multiIndexPartialDeriv_le {m : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (β : Fin m → ℕ) (f : EuclideanSpace ℝ (Fin m) → F) (x : EuclideanSpace ℝ (Fin m)) : ‖multiIndexPartialDeriv β f x‖ ≤ ‖iteratedFDeriv ℝ (multiIndexOrder β) f x‖

‖∂^β f(x)‖ ≤ ‖D^{|β|} f(x)‖ where D^k is the iterated Fréchet derivative.

theorem iteratedFDeriv_norm_le_sum_multiIndexPartialDeriv {m : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) (x : EuclideanSpace ℝ (Fin m)) : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ∑ σ : Fin n → Fin m, ‖MultiIndexBridge.multiIndexPartialDeriv (MultiIndexBridge.tupleToMultiIndex σ) (⇑f) x‖

The iterated Fréchet derivative norm of a Schwartz function is bounded by the sum over tuples of the corresponding mixed partial derivative norms.

theorem MultiIndexBridge.monomial_iteratedFDeriv_le_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) (x : EuclideanSpace ℝ (Fin m)) : |realMonomial α x| * ‖iteratedFDeriv ℝ (multiIndexOrder β) (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 (multiIndexOrder α) (multiIndexOrder β)) f

|x^α| · ‖D^{|β|} f(x)‖ is bounded by the Schwartz seminorm of order (|α|, |β|).

theorem MultiIndexBridge.norm_le_sum_abs {m : ℕ} (x : EuclideanSpace ℝ (Fin m)) : ‖x‖ ≤ ∑ i : Fin m, |x.ofLp i|

The Euclidean norm is bounded by the sum of coordinate absolute values: ‖x‖ ≤ ∑ |xᵢ|.

theorem MultiIndexBridge.norm_pow_le_sum_coord_pow {m : ℕ} (x : EuclideanSpace ℝ (Fin m)) (k : ℕ) : ‖x‖ ^ (k + 1) ≤ ↑m ^ k * ∑ i : Fin m, |x.ofLp i| ^ (k + 1)

Power-of-norm bound: ‖x‖^(k+1) ≤ m^k · ∑ |xᵢ|^(k+1) for x ∈ ℝ^m.

def MultiIndexBridge.coordMultiIndex {m : ℕ} (k : ℕ) (i : Fin m) : Fin m → ℕ

Single-coordinate multi-index: k at position i, zero elsewhere.

theorem MultiIndexBridge.multiIndexOrder_coordMultiIndex {m : ℕ} (k : ℕ) (i : Fin m) : multiIndexOrder (coordMultiIndex k i) = k

The order of the single-coordinate multi-index coordMultiIndex k i equals k.

theorem MultiIndexBridge.abs_coord_pow_eq_abs_realMonomial {m : ℕ} (x : EuclideanSpace ℝ (Fin m)) (i : Fin m) (k : ℕ) : |x.ofLp i| ^ k = |realMonomial (coordMultiIndex k i) x|

|xᵢ|^k = |x^{coordMultiIndex k i}|: a coordinate power matches the corresponding monomial.

def MultiIndexBridge.boundedMultiIndices (m K : ℕ) : Finset (Fin m → ℕ)

The finset of all multi-indices α : Fin m → ℕ with each αᵢ ≤ K.

theorem MultiIndexBridge.mem_boundedMultiIndices_iff {m : ℕ} (α : Fin m → ℕ) (K : ℕ) : α ∈ boundedMultiIndices m K ↔ ∀ (i : Fin m), α i ≤ K

Membership criterion: α ∈ boundedMultiIndices m K ↔ ∀ i, αᵢ ≤ K.

theorem MultiIndexBridge.mem_boundedMultiIndices_of_multiIndexOrder_le {m : ℕ} {α : Fin m → ℕ} {K : ℕ} (hα : multiIndexOrder α ≤ K) : α ∈ boundedMultiIndices m K

If the total order of α is at most K, then each coordinate is at most K.

theorem MultiIndexBridge.card_boundedMultiIndices (m K : ℕ) : (boundedMultiIndices m K).card = (K + 1) ^ m

Cardinality: there are (K + 1)^m multi-indices with each coordinate bounded by K.

def MultiIndexBridge.totalOrderBoundedMultiIndices (m K : ℕ) : Finset (Fin m → ℕ)

Multi-indices α with total order |α| ≤ K.

theorem MultiIndexBridge.mem_totalOrderBoundedMultiIndices_iff {m : ℕ} (α : Fin m → ℕ) (K : ℕ) : α ∈ totalOrderBoundedMultiIndices m K ↔ multiIndexOrder α ≤ K

Membership: α ∈ totalOrderBoundedMultiIndices m K ↔ |α| ≤ K.

theorem MultiIndexBridge.coordMultiIndex_mem_totalOrderBoundedMultiIndices {m : ℕ} (k : ℕ) (i : Fin m) (K : ℕ) (hk : k ≤ K) : coordMultiIndex k i ∈ totalOrderBoundedMultiIndices m K

coordMultiIndex k i belongs to totalOrderBoundedMultiIndices m K when k ≤ K.

theorem MultiIndexBridge.tupleToMultiIndex_mem_totalOrderBoundedMultiIndices {m n : ℕ} (σ : Fin n → Fin m) (K : ℕ) (hn : n ≤ K) : tupleToMultiIndex σ ∈ totalOrderBoundedMultiIndices m K

tupleToMultiIndex σ belongs to totalOrderBoundedMultiIndices m K whenever n ≤ K.

noncomputable def MultiIndexBridge.monomialDerivSupNorm {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : ℝ

The monomial-mixed-derivative sup norm: the infimum of c ≥ 0 with |x^α| · ‖∂^β f(x)‖ ≤ c for all x.

theorem MultiIndexBridge.monomialDerivSupNorm_bounds_nonempty {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : ∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (x : EuclideanSpace ℝ (Fin m)), |realMonomial α x| * ‖multiIndexPartialDeriv β (⇑f) x‖ ≤ c}

The set of bounds in monomialDerivSupNorm is nonempty, using Schwartz decay.

theorem MultiIndexBridge.monomialDerivSupNorm_bounds_bddBelow {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : EuclideanSpace ℝ (Fin m)), |realMonomial α x| * ‖multiIndexPartialDeriv β (⇑f) x‖ ≤ c}

The set of bounds in monomialDerivSupNorm is bounded below by 0.

theorem MultiIndexBridge.monomialDerivSupNorm_nonneg {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : 0 ≤ monomialDerivSupNorm α β f

monomialDerivSupNorm α β f is nonnegative.

theorem MultiIndexBridge.le_monomialDerivSupNorm {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) (x : EuclideanSpace ℝ (Fin m)) : |realMonomial α x| * ‖multiIndexPartialDeriv β (⇑f) x‖ ≤ monomialDerivSupNorm α β f

Pointwise: |x^α| · ‖∂^β f(x)‖ ≤ monomialDerivSupNorm α β f.

theorem MultiIndexBridge.monomialDerivSupNorm_le_bound {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : EuclideanSpace ℝ (Fin m)), |realMonomial α x| * ‖multiIndexPartialDeriv β (⇑f) x‖ ≤ M) : monomialDerivSupNorm α β f ≤ M

Any uniform pointwise bound M dominates monomialDerivSupNorm α β f.

theorem MultiIndexBridge.monomialDerivSupNorm_le_seminorm {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ} (α β : Fin m → ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : monomialDerivSupNorm α β f ≤ (SchwartzMap.seminorm 𝕜 (multiIndexOrder α) (multiIndexOrder β)) f

monomialDerivSupNorm α β f is bounded by the Schwartz seminorm of order (|α|, |β|).

noncomputable def MultiIndexBridge.bookMultiIndexNorm {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : ℝ

The book-style multi-index norm: sum of monomialDerivSupNorm α β f over all |α|, |β| ≤ K.

theorem MultiIndexBridge.bookMultiIndexNorm_nonneg {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : 0 ≤ bookMultiIndexNorm K f

bookMultiIndexNorm K f is nonnegative.

theorem MultiIndexBridge.bookMultiIndexNorm_le_monomialDerivNormSum {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ} (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : bookMultiIndexNorm K f ≤ ↑(((K + 1) ^ m) ^ 2) * TemperedDistributions.monomialDerivNormSum K f

Comparison: bookMultiIndexNorm K f ≤ ((K + 1)^m)^2 · monomialDerivNormSum K f.

theorem MultiIndexBridge.seminorm_le_bookMultiIndexNorm {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ} [Nonempty (Fin m)] {j n K : ℕ} (hj : j ≤ K) (hn : n ≤ K) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : (SchwartzMap.seminorm 𝕜 j n) f ≤ ↑m ^ (2 * K) * bookMultiIndexNorm K f

Reverse comparison: each Schwartz seminorm seminorm j n f with j, n ≤ K is at most m^{2K} · bookMultiIndexNorm K f.

theorem MultiIndexBridge.monomialDerivNormSum_le_bookMultiIndexNorm {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ} [Nonempty (Fin m)] (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : TemperedDistributions.monomialDerivNormSum K f ≤ ↑((K + 1) ^ 2) * ↑m ^ (2 * K) * bookMultiIndexNorm K f

Combined comparison: monomialDerivNormSum K f ≤ (K + 1)^2 · m^{2K} · bookMultiIndexNorm K f.

theorem MultiIndexBridge.weightedCkNormSup_equiv_bookMultiIndexNorm {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} (𝕜 : Type u_3) [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [Nonempty (Fin m)] (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin m)) F) : TemperedDistributions.weightedCkNormSup K f ≤ 2 ^ K * (↑((K + 1) ^ 2) * ↑m ^ (2 * K)) * bookMultiIndexNorm K f ∧ bookMultiIndexNorm K f ≤ ↑(((K + 1) ^ m) ^ 2) * ↑((K + 1) ^ 2) * TemperedDistributions.weightedCkNormSup K f

Equivalence of weightedCkNormSup and bookMultiIndexNorm up to constants depending on K and m.

theorem MultiIndexBridge.euclidean_sum_single_decomp {m : ℕ} (v : EuclideanSpace ℝ (Fin m)) : v = ∑ i : Fin m, v.ofLp i • EuclideanSpace.single i 1

Decomposition of a Euclidean vector into the sum v = ∑ᵢ vᵢ · eᵢ over the standard basis.

theorem MultiIndexBridge.multilinear_basis_expansion {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {m n : ℕ} (M : ContinuousMultilinearMap ℝ (fun (x : Fin n) => EuclideanSpace ℝ (Fin m)) F) (v : Fin n → EuclideanSpace ℝ (Fin m)) : M v = ∑ σ : Fin n → Fin m, (∏ k : Fin n, (v k).ofLp (σ k)) • M fun (k : Fin n) => EuclideanSpace.single (σ k) 1

Expansion of a continuous multilinear map M in the standard basis: M v = ∑_σ (∏ₖ v_k (σ k)) · M (e_{σ k}).

noncomputable def TemperedDistributions.japaneseBracketCkNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : ℝ

The ⟨x⟩^K-weighted C^k norm of a Schwartz function: the infimum of c ≥ 0 bounding ⟨x⟩^K · ‖∂^n f(x)‖ uniformly.

theorem TemperedDistributions.japaneseBracketCkNorm_bounds_nonempty {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : {c : ℝ | 0 ≤ c ∧ ∀ (x : E), japaneseBracket x ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}.Nonempty

The set of bounds for japaneseBracketCkNorm K n f is nonempty.

theorem TemperedDistributions.japaneseBracketCkNorm_bounds_bddBelow {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : E), japaneseBracket x ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

The set of bounds for japaneseBracketCkNorm K n f is bounded below by 0.

theorem TemperedDistributions.japaneseBracketCkNorm_nonneg {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : 0 ≤ japaneseBracketCkNorm K n f

japaneseBracketCkNorm K n f is nonnegative.

theorem TemperedDistributions.le_japaneseBracketCkNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) (x : E) : japaneseBracket x ^ K * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ japaneseBracketCkNorm K n f

Pointwise: ⟨x⟩^K · ‖∂^n f(x)‖ ≤ japaneseBracketCkNorm K n f.

theorem TemperedDistributions.japaneseBracketCkNorm_le_weightedCkNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : japaneseBracketCkNorm K n f ≤ weightedCkNorm K n f

japaneseBracketCkNorm K n f ≤ weightedCkNorm K n f.

theorem TemperedDistributions.weightedCkNorm_le_sqrt_two_pow_mul_japaneseBracketCkNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K n : ℕ) (f : SchwartzMap E F) : weightedCkNorm K n f ≤ √2 ^ K * japaneseBracketCkNorm K n f

Reverse: weightedCkNorm K n f ≤ (√2)^K · japaneseBracketCkNorm K n f.

noncomputable def TemperedDistributions.japaneseBracketCkNormSup {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ℕ) (f : SchwartzMap E F) : ℝ

The supremum of japaneseBracketCkNorm K n f over n ≤ K.

theorem TemperedDistributions.japaneseBracketCkNormSup_le_weightedCkNormSup {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ℕ) (f : SchwartzMap E F) : japaneseBracketCkNormSup K f ≤ weightedCkNormSup K f

japaneseBracketCkNormSup K f ≤ weightedCkNormSup K f.

theorem TemperedDistributions.weightedCkNormSup_le_sqrt_two_pow_mul_japaneseBracketCkNormSup {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ℕ) (f : SchwartzMap E F) : weightedCkNormSup K f ≤ √2 ^ K * japaneseBracketCkNormSup K f

Reverse: weightedCkNormSup K f ≤ (√2)^K · japaneseBracketCkNormSup K f.

theorem corollary_7_2_japaneseBracket_multiindex {𝕜 : Type u_1} [NormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {n : ℕ} [Nonempty (Fin n)] (K : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) : ∃ (C₁ : ℝ) (C₂ : ℝ), 0 < C₁ ∧ 0 < C₂ ∧ TemperedDistributions.japaneseBracketCkNormSup K f ≤ C₁ * MultiIndexBridge.bookMultiIndexNorm K f ∧ MultiIndexBridge.bookMultiIndexNorm K f ≤ C₂ * TemperedDistributions.japaneseBracketCkNormSup K f

Corollary 7.2 (Melrose): equivalence of the Japanese-bracket weighted C^K norm and the book multi-index norm up to constants C₁, C₂ > 0.