OAI/Combinatorics/HoneycombChords/EntireCosine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Calculus of the entire cosine continuation on the real line.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_sq line 12
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_zero line 14
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_neg_four line 15
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_contDiff line 17
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.hypJet_succ_zero line 22
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_sq_jet line 24
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.angle_pos line 38
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_sq line 39
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_sq_ne_zero line 41
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.g_sq line 46
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_eq_C line 63