OAI/Analysis/LiebThirring/RowSigns.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLiebThirring.ContinuationGap.LowerSpace line 15
  2. def OAI.SharpLiebThirring.ContinuationGap.rowSign line 18
  3. def OAI.SharpLiebThirring.ContinuationGap.signConjugate line 24
  4. def OAI.SharpLiebThirring.ContinuationGap.NonzeroRows line 27
  5. abbrev OAI.SharpLiebThirring.PathTopology.LowerIndex line 33
  6. abbrev OAI.SharpLiebThirring.PathTopology.lowerDim line 34
  7. def OAI.SharpLiebThirring.PathTopology.indexEquiv line 35
  8. def OAI.SharpLiebThirring.PathTopology.diagonalIndex line 37
  9. def OAI.SharpLiebThirring.PathTopology.rowIndex line 38
  10. def OAI.SharpLiebThirring.PathTopology.colIndex line 39
  11. lemma OAI.SharpLiebThirring.PathTopology.rowIndex_diagonal line 41
  12. lemma OAI.SharpLiebThirring.PathTopology.colIndex_diagonal line 43
  13. lemma OAI.SharpLiebThirring.PathTopology.colIndex_le_rowIndex line 45
  14. def OAI.SharpLiebThirring.PathTopology.lowerOfCoords line 50

    Source documentation

    Exact linear coordinates on the entire lower-triangular coefficient space; no nonvanishing or invertibility restriction is imposed.

    def lowerOfCoords {N : ℕ} (x : Fin (lowerDim N) → ℝ) : LowerSpace N :=
…

    Mentions: OAI.SharpLiebThirring.PathTopology.lowerDim

  15. def OAI.SharpLiebThirring.PathTopology.lowerCoords line 53
  16. lemma OAI.SharpLiebThirring.PathTopology.lowerCoords_lowerOfCoords line 56
  17. lemma OAI.SharpLiebThirring.PathTopology.lowerOfCoords_lowerCoords line 62
  18. lemma OAI.SharpLiebThirring.PathTopology.continuous_lowerCoords line 71
  19. lemma OAI.SharpLiebThirring.PathTopology.continuous_lowerOfCoords line 75
  20. def OAI.SharpLiebThirring.PathTopology.lowerHomeomorph line 85
  21. def OAI.SharpLiebThirring.PathTopology.rowSubgroup line 94

    Source documentation

    Coordinate reflections that flip whole rows and fix the homotopy time.

    def rowSubgroup (N : ℕ) : Subgroup (Signs (lowerDim N + 1)) where
…

    Mentions: OAI.SharpLiebThirring.PathTopology.lowerDim

  22. def OAI.SharpLiebThirring.PathTopology.rowBool line 102
  23. lemma OAI.SharpLiebThirring.PathTopology.rowSubgroup_time line 104
  24. lemma OAI.SharpLiebThirring.PathTopology.rowSubgroup_coord line 105
  25. lemma OAI.SharpLiebThirring.PathTopology.rowBool_one line 108
  26. lemma OAI.SharpLiebThirring.PathTopology.rowBool_mul line 109
  27. lemma OAI.SharpLiebThirring.PathTopology.rowBool_injective line 112
  28. def OAI.SharpLiebThirring.PathTopology.rowElement line 121
  29. lemma OAI.SharpLiebThirring.PathTopology.rowBool_rowElement line 127
  30. def OAI.SharpLiebThirring.PathTopology.signValue line 131
  31. lemma OAI.SharpLiebThirring.PathTopology.signValue_false line 132
  32. lemma OAI.SharpLiebThirring.PathTopology.signValue_true line 133
  33. lemma OAI.SharpLiebThirring.PathTopology.signValue_cases line 134
  34. lemma OAI.SharpLiebThirring.PathTopology.signValue_xor line 135
  35. lemma OAI.SharpLiebThirring.PathTopology.signValue_smul line 137
  36. def OAI.SharpLiebThirring.PathTopology.conjugateSigns line 140
  37. def OAI.SharpLiebThirring.PathTopology.conjugateRepresentation line 143
  38. lemma OAI.SharpLiebThirring.PathTopology.conjugateRepresentation_norm line 161
  39. lemma OAI.SharpLiebThirring.PathTopology.conjugateRepresentation_apply line 163
  40. def OAI.SharpLiebThirring.PathTopology.matrixCoords line 175

    Source documentation

    Lower-coordinate restriction is faithful on symmetric matrices.

    def matrixCoords {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) : Fin (lowerDim N) → ℝ :=
…

    Mentions: OAI.SharpLiebThirring.PathTopology.lowerDim

  41. lemma OAI.SharpLiebThirring.PathTopology.continuous_matrixCoords line 177
  42. lemma OAI.SharpLiebThirring.PathTopology.matrixCoords_eq_zero line 181
  43. def OAI.SharpLiebThirring.PathTopology.diagonalLower line 192
  44. def OAI.SharpLiebThirring.PathTopology.diagonalPoint line 194
  45. lemma OAI.SharpLiebThirring.PathTopology.lowerOfCoords_diagonalPoint line 195
  46. def OAI.SharpLiebThirring.PathTopology.lowerEntry line 198
  47. lemma OAI.SharpLiebThirring.PathTopology.lowerEntry_apply line 200
  48. lemma OAI.SharpLiebThirring.PathTopology.lowerEntry_diagonal line 204
  49. def OAI.SharpLiebThirring.PathTopology.initialMap line 209
  50. def OAI.SharpLiebThirring.PathTopology.jacobianWeight line 212
  51. lemma OAI.SharpLiebThirring.PathTopology.jacobianWeight_ne_zero line 214
  52. def OAI.SharpLiebThirring.PathTopology.initialLinearEquiv line 223
  53. lemma OAI.SharpLiebThirring.PathTopology.initialLinearEquiv_apply line 227
  54. lemma OAI.SharpLiebThirring.PathTopology.initialMap_hasFDerivAt line 231
  55. def OAI.SharpLiebThirring.PathTopology.spaceTimeHomeomorph line 282
  56. def OAI.SharpLiebThirring.PathTopology.clampTime line 300
  57. lemma OAI.SharpLiebThirring.PathTopology.continuous_clampTime line 301
  58. lemma OAI.SharpLiebThirring.PathTopology.clampTime_mem line 302
  59. lemma OAI.SharpLiebThirring.PathTopology.clampTime_eq line 304
  60. lemma OAI.SharpLiebThirring.PathTopology.clampTime_zero line 306
  61. lemma OAI.SharpLiebThirring.PathTopology.clampTime_one line 307
  62. def OAI.SharpLiebThirring.PathTopology.homotopyCoords line 309
  63. lemma OAI.SharpLiebThirring.PathTopology.continuous_homotopyCoords line 312
  64. lemma OAI.SharpLiebThirring.PathTopology.lowerOfCoords_smul line 321
  65. lemma OAI.SharpLiebThirring.PathTopology.time_smul line 338
  66. lemma OAI.SharpLiebThirring.PathTopology.homotopyCoords_equivariant line 344
  67. lemma OAI.SharpLiebThirring.PathTopology.homotopyCoords_eq_zero line 355
  68. lemma OAI.SharpLiebThirring.PathTopology.compact_homotopyCoords_zeros line 366
  69. lemma OAI.SharpLiebThirring.PathTopology.rowAction_free line 380
  70. lemma OAI.SharpLiebThirring.PathTopology.homotopyCoords_initial line 395
  71. lemma OAI.SharpLiebThirring.PathTopology.initial_matrix_zero line 411
  72. lemma OAI.SharpLiebThirring.PathTopology.gram_of_initial_zero line 426
  73. lemma OAI.SharpLiebThirring.PathTopology.homotopyCoords_initial_orbit line 440
  74. theorem OAI.SharpLiebThirring.PathTopology.equivariant_continuation line 486

    Source documentation

    Row-sign continuation. Rank deficiency is allowed throughout; only zero rows at matching solutions are excluded.

    theorem equivariant_continuation (N : ℕ) (ε : ℝ) (k : Fin N → ℝ)
    (hε : 0 < ε) (hk : ∀ i, 0 < k i)
    (Φ : ℝ → LowerSpace N → Matrix (Fin N) (Fin N) ℝ)
    (hΦ : ContinuousOn (fun z : LowerSpace N × ℝ ↦ Φ z.2 z.1) (Set.univ ×ˢ Set.Icc 0 1))
    (hs : ∀ θ ∈ Set.Icc (0 : ℝ) 1, ∀ C, (Φ θ C).IsHermitian)
    (he : ∀ θ ∈ Set.Icc (0 : ℝ) 1, ∀ C, ∀ s : Fin N → ℝ,
      (∀ i, s i = 1 ∨ s i = -1) → Φ θ (rowSign s C) = signConjugate s (Φ θ C))
    (h0 : ∀ C, Φ 0 C = 2 • diagonal k - ε⁻¹ • (C.val * C.val.transpose))
    (hK : IsCompact {z : LowerSpace N × ℝ | z.2 ∈ Set.Icc (0 : ℝ) 1 ∧ Φ z.2 z.1 = 0})
    (hn : ∀ θ ∈ Set.Icc (0 : ℝ) 1, ∀ C, Φ θ C = 0 → NonzeroRows C) :
    ∃ C, Φ 1 C = 0 := by
…