OAI/Combinatorics/HoneycombChords/ConfluentInterpolation.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Confluent spectral zeros and physical rational interpolation.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiff_sine line 15
  2. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiff_Q line 18
  3. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiff_bulkNumerator line 22
  4. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiffAt_spectralR line 27
  5. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiffAt_boundary0 line 30
  6. lemma OAI.CriticalHoneycomb.Transfer.Reflection.contDiffAt_boundary1 line 41
  7. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.contDiffAt_matrix_entry line 58
  8. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.contDiffAt_row line 62
  9. lemma OAI.CriticalHoneycomb.BoundaryJet.base_sub line 84
  10. lemma OAI.CriticalHoneycomb.BoundaryJet.left_sub line 85
  11. lemma OAI.CriticalHoneycomb.BoundaryJet.right_sub line 86
  12. lemma OAI.CriticalHoneycomb.BoundaryJet.both_sub line 87
  13. def OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt line 89
  14. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.const line 94
  15. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.add line 96
  16. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.sub line 104
  17. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.mul line 112
  18. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.sum line 121
  19. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.C line 128
  20. lemma OAI.CriticalHoneycomb.BoundaryJet.SmoothJetAt.reflect line 132
  21. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.contDiffAt_row_curve line 150
  22. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.contDiffAt_bulkRows_curve line 157
  23. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_K line 170
  24. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_T_curve line 178
  25. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_reorient line 188
  26. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_commonScalar line 193
  27. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_matrix_mul line 202
  28. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.fusionDefect line 221
  29. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.FusionRegular line 224
  30. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect line 226
  31. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.centered_T_reflect line 228
  32. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.fusionRegular_neg line 233
  33. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.fusionDefect_reflect line 241
  34. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.fusionDefect_node line 251
  35. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_node line 261
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_reflect line 267
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.reorient_sub line 271
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.commonScalar_sub line 275
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_homogeneous line 279
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smoothJetAt_fusionDefect line 292
  41. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.contDiffAt_physicalDefect line 306
  42. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.L_pos line 320
  43. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.nonsingular_core line 321
  44. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.perturb line 336
  45. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.radius line 337
  46. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.radius_pos line 338
  47. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.radius_mul line 339
  48. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.perturb_zero line 343
  49. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.perturb_core line 344
  50. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.perturb_regular line 359
  51. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.zeroSlope line 377
  52. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.zeroSlope_strict line 379
  53. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.zeroSlope_bound line 384
  54. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.zeroSlope_signed line 390
  55. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.perturb_signed_zero line 405
  56. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.affine_node_close line 417
  57. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.smooth_perturb_defect line 421
  58. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_zero_jets line 427
  59. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_L_jets line 447
  60. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalDefect_eventually line 474
  61. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP_zero_fusion_jets line 486
  62. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP_L_fusion_jets line 491
  63. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polePoly_eval line 503
  64. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalNumerator_eval line 507
  65. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.interpolationDenominator_ne line 517
  66. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.interpolant_is_physical line 526
  67. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.interpolant_is_physical_interval line 538
  68. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.interpolant_fusion_eventually line 545
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.bridgeMass_actual_tsum line 566
  70. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_physical_spectral_interpolation line 575