Weighted ℓ¹ coefficient infrastructure

The ordinary complex norm is not ultrametric. We therefore work with honest ℓ¹ coefficient estimates: antidiagonal convolution is submultiplicative, high shifts and low cuts have operator norm at most one, and evaluation on the unit polydisc is bounded by the ℓ¹ norm.

@[reducible, inline]

noncomputable abbrev ClassicalComplexWPT.L1Coeff (I : Type u_1) : AddSubgroup (PreLp fun (x : I) => ℂ)

Complex ℓ¹ coefficients indexed by I.

Equations

• ClassicalComplexWPT.L1Coeff I = lp (fun (x : I) => ℂ) 1

theorem ClassicalComplexWPT.L1Coeff.summable_norm {I : Type u_1} (f : ↥(L1Coeff I)) : Summable fun (i : I) => ‖↑f i‖

theorem ClassicalComplexWPT.L1Coeff.norm_eq_tsum_norm {I : Type u_1} (f : ↥(L1Coeff I)) : ‖f‖ = ∑' (i : I), ‖↑f i‖

def ClassicalComplexWPT.convolutionFun {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) (n : A) : ℂ

Antidiagonal Cauchy product of two ℓ¹ coefficient families.

Equations

• ClassicalComplexWPT.convolutionFun f g n = ∑ kl ∈ Finset.antidiagonal n, ↑f kl.1 * ↑g kl.2

theorem ClassicalComplexWPT.summable_antidiagonal_norm_product {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) : Summable fun (n : A) => ∑ kl ∈ Finset.antidiagonal n, ‖↑f kl.1‖ * ‖↑g kl.2‖

theorem ClassicalComplexWPT.summable_norm_convolutionFun {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) : Summable fun (n : A) => ‖convolutionFun f g n‖

def ClassicalComplexWPT.convolution {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) : ↥(L1Coeff A)

Antidiagonal convolution as an ℓ¹ coefficient family.

Equations

• ClassicalComplexWPT.convolution f g = ⟨ClassicalComplexWPT.convolutionFun f g, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.convolution_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) (n : A) : ↑(convolution f g) n = ∑ kl ∈ Finset.antidiagonal n, ↑f kl.1 * ↑g kl.2

theorem ClassicalComplexWPT.norm_convolution_le {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) : ‖convolution f g‖ ≤ ‖f‖ * ‖g‖

The ordinary ℓ¹ Cauchy-product estimate.

theorem ClassicalComplexWPT.convolution_add_left {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f₁ f₂ g : ↥(L1Coeff A)) : convolution (f₁ + f₂) g = convolution f₁ g + convolution f₂ g

theorem ClassicalComplexWPT.convolution_smul_left {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (c : ℂ) (f g : ↥(L1Coeff A)) : convolution (c • f) g = c • convolution f g

def ClassicalComplexWPT.convolutionRightLinear {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (g : ↥(L1Coeff A)) : ↥(L1Coeff A) →ₗ[ℂ] ↥(L1Coeff A)

Right convolution as a linear map.

Equations

• ClassicalComplexWPT.convolutionRightLinear g = { toFun := fun (f : ↥(ClassicalComplexWPT.L1Coeff A)) => ClassicalComplexWPT.convolution f g, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ClassicalComplexWPT.convolutionRight {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (g : ↥(L1Coeff A)) : ↥(L1Coeff A) →L[ℂ] ↥(L1Coeff A)

Right convolution as a continuous linear map.

Equations

• ClassicalComplexWPT.convolutionRight g = (ClassicalComplexWPT.convolutionRightLinear g).mkContinuous ‖g‖ ⋯

@[simp]

theorem ClassicalComplexWPT.convolutionRight_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (g f : ↥(L1Coeff A)) : (convolutionRight g) f = convolution f g

theorem ClassicalComplexWPT.norm_convolutionRight_le {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (g : ↥(L1Coeff A)) : ‖convolutionRight g‖ ≤ ‖g‖

def ClassicalComplexWPT.highIndex {A : Type u_1} (d : ℕ) : A × ℕ → A × ℕ

Index map which discards the first d distinguished-variable coefficients.

Equations

• ClassicalComplexWPT.highIndex d x = (x.1, x.2 + d)

theorem ClassicalComplexWPT.highIndex_injective {A : Type u_1} (d : ℕ) : Function.Injective (highIndex d)

def ClassicalComplexWPT.highShift {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Delete the first d distinguished-variable coefficient layers.

Equations

• ClassicalComplexWPT.highShift d f = ⟨fun (x : A × ℕ) => ↑f (ClassicalComplexWPT.highIndex d x), ⋯⟩

@[simp]

theorem ClassicalComplexWPT.highShift_apply {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) (n : ℕ) : ↑(highShift d f) (a, n) = ↑f (a, n + d)

theorem ClassicalComplexWPT.norm_highShift_le {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : ‖highShift d f‖ ≤ ‖f‖

theorem ClassicalComplexWPT.highShift_add {A : Type u_1} (d : ℕ) (f g : ↥(L1Coeff (A × ℕ))) : highShift d (f + g) = highShift d f + highShift d g

theorem ClassicalComplexWPT.highShift_smul {A : Type u_1} (d : ℕ) (c : ℂ) (f : ↥(L1Coeff (A × ℕ))) : highShift d (c • f) = c • highShift d f

def ClassicalComplexWPT.highShiftLinear {A : Type u_1} (d : ℕ) : ↥(L1Coeff (A × ℕ)) →ₗ[ℂ] ↥(L1Coeff (A × ℕ))

High shift as a complex-linear map.

Equations

• ClassicalComplexWPT.highShiftLinear d = { toFun := ClassicalComplexWPT.highShift d, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ClassicalComplexWPT.highShiftCLM {A : Type u_1} (d : ℕ) : ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

High shift as a contraction.

Equations

• ClassicalComplexWPT.highShiftCLM d = (ClassicalComplexWPT.highShiftLinear d).mkContinuous 1 ⋯

theorem ClassicalComplexWPT.norm_highShiftCLM_le {A : Type u_1} (d : ℕ) : ‖highShiftCLM d‖ ≤ 1

def ClassicalComplexWPT.lowCut {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Keep exactly the distinguished-variable coefficient layers below d.

Equations

• ClassicalComplexWPT.lowCut d f = ⟨fun (x : A × ℕ) => if x.2 < d then ↑f x else 0, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.lowCut_apply_of_lt {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) {n : ℕ} (hn : n < d) : ↑(lowCut d f) (a, n) = ↑f (a, n)

@[simp]

theorem ClassicalComplexWPT.lowCut_apply_of_le {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) {n : ℕ} (hn : d ≤ n) : ↑(lowCut d f) (a, n) = 0

theorem ClassicalComplexWPT.norm_lowCut_le {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : ‖lowCut d f‖ ≤ ‖f‖

theorem ClassicalComplexWPT.lowCut_add {A : Type u_1} (d : ℕ) (f g : ↥(L1Coeff (A × ℕ))) : lowCut d (f + g) = lowCut d f + lowCut d g

theorem ClassicalComplexWPT.lowCut_smul {A : Type u_1} (d : ℕ) (c : ℂ) (f : ↥(L1Coeff (A × ℕ))) : lowCut d (c • f) = c • lowCut d f

def ClassicalComplexWPT.lowCutLinear {A : Type u_1} (d : ℕ) : ↥(L1Coeff (A × ℕ)) →ₗ[ℂ] ↥(L1Coeff (A × ℕ))

Low-degree cutoff as a complex-linear map.

Equations

• ClassicalComplexWPT.lowCutLinear d = { toFun := ClassicalComplexWPT.lowCut d, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ClassicalComplexWPT.lowCutCLM {A : Type u_1} (d : ℕ) : ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

Low cutoff as a contraction.

Equations

• ClassicalComplexWPT.lowCutCLM d = (ClassicalComplexWPT.lowCutLinear d).mkContinuous 1 ⋯

theorem ClassicalComplexWPT.norm_lowCutCLM_le {A : Type u_1} (d : ℕ) : ‖lowCutCLM d‖ ≤ 1

def ClassicalComplexWPT.monomial {S : Type u_1} (y : S → ℂ) (a : S →₀ ℕ) : ℂ

A multivariate monomial indexed by a finitely-supported exponent vector.

Equations

• ClassicalComplexWPT.monomial y a = a.prod fun (i : S) (n : ℕ) => y i ^ n

@[simp]

theorem ClassicalComplexWPT.monomial_zero {S : Type u_1} (y : S → ℂ) : monomial y 0 = 1

theorem ClassicalComplexWPT.monomial_add {S : Type u_1} (y : S → ℂ) (a b : S →₀ ℕ) : monomial y (a + b) = monomial y a * monomial y b

theorem ClassicalComplexWPT.norm_monomial_le_one {S : Type u_1} (y : S → ℂ) (hy : ∀ (i : S), ‖y i‖ ≤ 1) (a : S →₀ ℕ) : ‖monomial y a‖ ≤ 1

def ClassicalComplexWPT.monomialWeight {S : Type u_1} (r : S → ℝ) (a : S →₀ ℕ) : ℝ

Multiplicative real polyradius weight.

Equations

• ClassicalComplexWPT.monomialWeight r a = a.prod fun (i : S) (n : ℕ) => r i ^ n

theorem ClassicalComplexWPT.monomialWeight_add {S : Type u_1} (r : S → ℝ) (a b : S →₀ ℕ) : monomialWeight r (a + b) = monomialWeight r a * monomialWeight r b

noncomputable def ClassicalComplexWPT.evalL1 {S : Type u_1} (f : ↥(L1Coeff (S →₀ ℕ))) (y : S → ℂ) : ℂ

Evaluate an ℓ¹ coefficient family on the unit polydisc.

Equations

• ClassicalComplexWPT.evalL1 f y = ∑' (a : S →₀ ℕ), ↑f a * ClassicalComplexWPT.monomial y a

theorem ClassicalComplexWPT.summable_norm_evalL1_terms {S : Type u_1} (f : ↥(L1Coeff (S →₀ ℕ))) (y : S → ℂ) (hy : ∀ (i : S), ‖y i‖ ≤ 1) : Summable fun (a : S →₀ ℕ) => ‖↑f a * monomial y a‖

theorem ClassicalComplexWPT.summable_evalL1_terms {S : Type u_1} (f : ↥(L1Coeff (S →₀ ℕ))) (y : S → ℂ) (hy : ∀ (i : S), ‖y i‖ ≤ 1) : Summable fun (a : S →₀ ℕ) => ↑f a * monomial y a

theorem ClassicalComplexWPT.norm_evalL1_le {S : Type u_1} (f : ↥(L1Coeff (S →₀ ℕ))) (y : S → ℂ) (hy : ∀ (i : S), ‖y i‖ ≤ 1) : ‖evalL1 f y‖ ≤ ‖f‖

Evaluation on the unit polydisc is bounded by the coefficient ℓ¹ norm.