OAI/Analysis/Triangular/Energy/Spectral.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularUniversal.phase line 12

   Source comment

   Necessary analytic transfer from §2. We use finite positive measures for the comparison form; the eventual quadratic inequality also handles real signed linear combinations, without imposing spacing on the configuration.

   def phase (w x : Plane) : ℂ := Complex.exp ((2 * Real.pi * ⟪w, x⟫ : ℝ) * I)

   Mentions: OAI.TriangularUniversal.Plane

2. def OAI.TriangularUniversal.pattern line 13
3. def OAI.TriangularUniversal.kernelForm line 16
4. lemma OAI.TriangularUniversal.phase_continuous line 19
5. lemma OAI.TriangularUniversal.phase_norm line 23
6. lemma OAI.TriangularUniversal.phase_sub line 26
7. lemma OAI.TriangularUniversal.pattern_eq line 33
8. lemma OAI.TriangularUniversal.pattern_continuous line 40
9. lemma OAI.TriangularUniversal.pattern_bound line 45
10. lemma OAI.TriangularUniversal.spectral_integrable line 48
11. lemma OAI.TriangularUniversal.integral_phase_sub line 56
12. lemma OAI.TriangularUniversal.kernelForm_spectral line 64
13. lemma OAI.TriangularUniversal.integral_reC line 93
14. lemma OAI.TriangularUniversal.integral_sub_sub_add line 97
15. lemma OAI.TriangularUniversal.spectral_re_nonneg line 108
16. lemma OAI.TriangularUniversal.kernelForm_diag_re_nonneg line 114
17. lemma OAI.TriangularUniversal.kernelForm_comparison line 121