delta

formal source

  17namespace Ndim
  18
  19/-- The Kronecker delta on `Fin n`. -/
  20def delta {n : ℕ} (i j : Fin n) : ℝ :=
  21  if i = j then 1 else 0
  22
  23/-- The flat affine connection in `x`-coordinates. -/
  24def xFlatConnection {n : ℕ} (_x : Vec n) (_i _j _k : Fin n) : ℝ := 0
  25
  26/-- The flat `t`-connection pulled back through `tᵢ = log xᵢ`. -/
  27noncomputable def tPulledConnection {n : ℕ} (x : Vec n) (i j k : Fin n) : ℝ :=
  28  if i = j ∧ j = k then -(x i)⁻¹ else 0
  29
  30/-- Projective equivalence to the zero connection. -/
  31def ProjectivelyEquivalentToZeroAt {n : ℕ}
  32    (Γ : Fin n → Fin n → Fin n → ℝ) : Prop :=
  33  ∃ ψ : Vec n, ∀ i j k : Fin n,
  34    Γ i j k = delta i j * ψ k + delta i k * ψ j
  35
  36@[simp] theorem xFlatConnection_apply {n : ℕ} (x : Vec n) (i j k : Fin n) :
  37    xFlatConnection x i j k = 0 := rfl
  38
  39theorem tPulledConnection_diag {n : ℕ} (x : Vec n) (i : Fin n) :
  40    tPulledConnection x i i i = -(x i)⁻¹ := by
  41  unfold tPulledConnection
  42  simp
  43
  44theorem tPulledConnection_offDiag {n : ℕ} (x : Vec n) {i j k : Fin n}
  45    (hijk : ¬ (i = j ∧ j = k)) :
  46    tPulledConnection x i j k = 0 := by
  47  unfold tPulledConnection
  48  simp [hijk]
  49
  50theorem projectivelyEquivalent_one_dim {x : Vec 1} :