OAI/Dynamics/ThreeTorus/PacketAlgebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeTorus.PassagePackets.reindex line 18
2. lemma OAI.ThreeTorus.PassagePackets.reindex_good line 44
3. lemma OAI.ThreeTorus.PassagePackets.reindex_reflection line 47
4. def OAI.ThreeTorus.PassagePackets.append line 57

   Source documentation

   Two arbitrary smooth packet lists in the SAME good arc and speed may be merged. The coefficient supports are not required to be disjoint.

   def append (F : PassagePackets ι) (G : PassagePackets κ) {δ : ℝ}
       (hδ : 0 ≤ δ) (hF : F.GoodArc δ) (hG : G.GoodArc δ) (_hV : G.V=F.V) :
       PassagePackets (ι ⊕ κ) := by
   …

   Mentions: OAI.ThreeTorus.PassagePackets

5. lemma OAI.ThreeTorus.PassagePackets.append_good line 129
6. lemma OAI.ThreeTorus.PassagePackets.append_reflection line 134
7. def OAI.ThreeTorus.PassagePackets.regroup line 151

   Source documentation

   Finite regrouping of amplitudes. Used only for equal-mode terms; this constructor does not assert an orthogonality or spectral identity.

   def regroup [Fintype ι] (F : PassagePackets ι) (s : κ → Finset ι)
       (m : κ → ℤ) (hm : ∀ i, m i ≠ 0) (c : κ → ι → ℂ) : PassagePackets κ where
   …

   Mentions: OAI.ThreeTorus.PassagePackets

8. def OAI.ThreeTorus.physicalDist line 207
9. lemma OAI.ThreeTorus.physicalDist_nonneg line 208
10. lemma OAI.ThreeTorus.physicalDist_sq line 209
11. lemma OAI.ThreeTorus.physicalDist_lt_iff line 211
12. lemma OAI.ThreeTorus.physicalDist_symm line 213
13. lemma OAI.ThreeTorus.physicalDist_chart line 215
14. lemma OAI.ThreeTorus.physicalDist_equiv line 220
15. lemma OAI.ThreeTorus.norm_toLp_sq line 224
16. lemma OAI.ThreeTorus.physicalError_eq_norm line 233
17. lemma OAI.ThreeTorus.physicalDist_eq_norm line 238
18. lemma OAI.ThreeTorus.physicalDist_triangle line 242
19. lemma OAI.ThreeTorus.physicalDist_finsum line 247