OAI/NumberTheory/Ostmann/Characters/TensorKernelEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.tensorKernel line 10
2. theorem OAI.Ostmann.tensorKernel_energy_le line 16

   Source documentation

   Slice first in one coordinate and then in the other. The two operator bounds multiply; the cardinalities of the coordinate spaces never enter.

   theorem tensorKernel_energy_le {α β γ δ : Type*}
       [Fintype α] [Fintype β] [Fintype γ] [Fintype δ]
       (M : α → β → ℂ) (N : γ → δ → ℂ) (A B : ℝ)
       (hM : ∀ f : β → ℂ, (∑ x, ‖∑ y, M x y * f y‖ ^ 2) ≤ A ^ 2 * ∑ y, ‖f y‖ ^ 2)
       (hN : ∀ f : δ → ℂ, (∑ x, ‖∑ y, N x y * f y‖ ^ 2) ≤ B ^ 2 * ∑ y, ‖f y‖ ^ 2)
       (f : β × δ → ℂ) :
       (∑ x, ‖∑ y, tensorKernel M N x y * f y‖ ^ 2) ≤
         (A * B) ^ 2 * ∑ y, ‖f y‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.tensorKernel