OAI/NumberTheory/Ostmann/Supply/FiniteTensorKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.kernel_energy_reindex line 13
2. def OAI.Ostmann.finiteTensorKernel line 27
3. theorem OAI.Ostmann.finiteTensorKernel_energy_le line 32

   Source documentation

   Iterating the two-factor bound never introduces the sizes of the residue fields.

   theorem finiteTensorKernel_energy_le {n : ℕ}
       (α : Fin n → Type u) (β : Fin n → Type v)
       [∀ i, Fintype (α i)] [∀ i, Fintype (β i)]
       (M : ∀ i, α i → β i → ℂ) (A : Fin n → ℝ)
       (hM : ∀ i (f : β i → ℂ), (∑ x, ‖∑ y, M i x y * f y‖ ^ 2) ≤ A i ^ 2 * ∑ y, ‖f y‖ ^ 2)
       (f : (∀ i, β i) → ℂ) :
       (∑ x, ‖∑ y, finiteTensorKernel M x y * f y‖ ^ 2) ≤
         (∏ i, A i) ^ 2 * ∑ y, ‖f y‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.finiteTensorKernel

4. theorem OAI.Ostmann.finiteTensorKernel_pairing line 53

   Source documentation

   Tensor coordinates evaluate as the product of the local kernel pairings.

   theorem finiteTensorKernel_pairing {ι : Type*} [Fintype ι]
       {α : ι → Type u} {β : ι → Type v}
       [∀ i, Fintype (α i)] [∀ i, Fintype (β i)]
       (M : ∀ i, α i → β i → ℂ) (a : ∀ i, α i → ℂ) (b : ∀ i, β i → ℂ) :
       (∑ x, conj (∏ i, a i (x i)) * ∑ y, finiteTensorKernel M x y * ∏ i, b i (y i)) =
         ∏ i, ∑ x, conj (a i x) * ∑ y, M i x y * b i y := by
   …

   Mentions: OAI.Ostmann.finiteTensorKernel