OAI/Combinatorics/HoneycombChords/ConfluentZeros.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coalescing real and complex zeros through Rolle's theorem.

The affine specialization gives vanishing jets when distinct zeros converge to one point.

  1. lemma OAI.CriticalHoneycomb.Analysis.rolle_many line 13
  2. lemma OAI.CriticalHoneycomb.Analysis.confluent_zero line 41
  3. lemma OAI.CriticalHoneycomb.Analysis.contDiffAt_partial_deriv line 68
  4. lemma OAI.CriticalHoneycomb.Analysis.contDiffAt_partial_iteratedDeriv line 81
  5. lemma OAI.CriticalHoneycomb.Analysis.confluent_zero_eventually line 97
  6. lemma OAI.CriticalHoneycomb.Analysis.confluent_affine line 122
  7. lemma OAI.CriticalHoneycomb.Analysis.iteratedDeriv_clm line 156
  8. lemma OAI.CriticalHoneycomb.Analysis.confluent_affine_complex line 165