OAI/Combinatorics/HoneycombChords/PositivePencils.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Oblique comparison and noncoincidence for the strip jet pencils.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetRectPencil line 11
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetRectPencil_square line 14
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetRectPencil_transpose line 16
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetRectPencil_vecMul line 23
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetRectPencil_vecMul_nonzero line 40
  6. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil line 59
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_transpose line 62
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_corner line 66
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_vecMul line 73
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_left_nonzero line 85
  11. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_knotPencil_no_common_root line 101
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram_isHermitian line 122
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram_quadratic line 129
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram_posDef line 148
  15. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_symmetric_jet_pencil_factors line 163

    Source documentation

    The symmetric M pencil has only positive real roots.

    theorem pole_symmetric_jet_pencil_factors {n : ℕ} (b : ℕ → ℝ) {z : ℝ} (hz : 0<z)
    (hb : Monotone (fun i : Fin n=>b i)) (hb0 : ∀ i : Fin n,0 ≤ b i)
    (hb1 : ∀ i : Fin n,b i ≤ angle^2) :
    ∃ e : Fin n → ℝ,(∀ i,0<e i) ∧ ∀ t : ℝ,
      (jetPencil (n:=n) (poleAdjustedDensity z) b b t).det=
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPencil, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleAdjustedDensity

  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetPencil_affine line 197
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetGram_det_pos line 207
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetGram_posDef line 215
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetPencil_zero_posDef line 222
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_cosh_moment_continuousOn line 239
  21. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPairing line 294
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPairing_continuousOn line 298
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_vecMul_last line 305
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPairing_ne_zero line 318
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuousOn_nonzero_mul_pos line 336
  26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPairing_product_pos line 360

    Source documentation

    The residues of the actual first-chain oblique Schur complement have the symmetric sign. This avoids assuming complex-root reality or interlacing.

    theorem knotPairing_product_pos (N : ℕ) {z : ℝ} (hz : 0<z) (a : Fin (2*N) → ℝ) (ha : a≠0) (r : ℝ)
    (har : a ᵥ* jetPencil (n:=2*N) (poleAdjustedDensity z) (twoKnotLabels N) (twoKnotLabels N) r=0)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPencil, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleAdjustedDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnotLabels

  27. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotGram line 374
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotGram_corner line 377
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_affine line 384
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotPencil_det_pos_nonpos line 393
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reorderedKnotGram_det_pos line 402
  32. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_knot_characteristic_comparison line 420
  33. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.first_oblique_characteristic_comparison line 461

    Source documentation

    The previously open exact target, at its literal F_s with s=L/2.

    theorem first_oblique_characteristic_comparison : FirstObliqueCharacteristicComparison := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.FirstObliqueCharacteristicComparison

  34. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet line 475

    Source documentation

    Remove the constant row and subtract evaluation at zero from every remaining complete jet. When b 0=0 these are an exact basis of ker(ev₀).

    noncomputable def zeroJet (b : ℕ → ℝ) (i : ℕ) (x : ℝ) : ℝ :=
…
  35. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnotLabels line 479
  36. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetPencil line 481
  37. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedZeroJetPencil line 484
  38. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SecondObliqueCharacteristicComparison line 489
  39. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination line 507
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_first_constant line 509
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_eq_zeroCombination line 512
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination_smul line 521
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetTest_zero_at_zero line 527
  44. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_jet_flag_sign_matching line 537

    Source documentation

    The zero-at-the-origin flag has a sign-matching test for each continuous function with fewer positive zeros than its dimension. This is the exact flag used in the second oblique chain, not an additional Chebyshev input.

    theorem zero_jet_flag_sign_matching {m : ℕ} (b : ℕ → ℝ) (f : ℝ → ℝ)
    (hb : Monotone (fun i : Fin (m+1)=>b i)) (hb0 : ∀ i : Fin (m+1),0  ≤  b i)
    (hbfirst : b 0 = 0) (hf : Continuous f) (s : Finset ℝ) (hs : ∀ x  ∈  s,0 < x)
    (hz : ∀ x,0 < x → (f x=0  ↔  x ∈ s)) (hc : s.card < m) :
    ∃ k : ℕ,k+1 ≤ m ∧ ∃ a : Fin (k+1) → ℝ,
      (∀ x,0 < x → 0 ≤ f x*zeroJetCombination b a x) ∧
      (∀ x,0 < x → f x ≠ 0 → 0 < f x*zeroJetCombination b a x) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination