1. Physlib
  2. Relativity
  3. LorentzGroup
  4. Boosts
  5. Basic
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.LorentzGroup.Basic

Boosts in the Lorentz group

@[expose] public section

The Lorentz factor (aka gamma factor or Lorentz term).

def γ (β : ℝ) : ℝ := 1 / Real.sqrt (1 - β^2)
lemma γ_sq (β : ℝ) (hβ : |β| < 1) : (γ β)^2 = 1 / (1 - β^2) := β:ℝhβ:|β| < 1⊢ γ β ^ 2 = 1 / (1 - β ^ 2) β:ℝhβ:|β| < 1⊢ √(1 - β ^ 2) ^ 2 = 1 - β ^ 2 β:ℝhβ:|β| < 1⊢ 0 ≤ 1 - β ^ 2 β:ℝhβ:|β| < 1⊢ |β| ≤ 1 All goals completed! 🐙@[simp] lemma γ_zero : γ 0 = 1 := ⊢ γ 0 = 1 All goals completed! 🐙@[simp] lemma γ_neg (β : ℝ) : γ (-β) = γ β := β:ℝ⊢ γ (-β) = γ β All goals completed! 🐙β:ℝhβ:-1 < β ∧ β < 1hn:1 - β ^ 2 = 0h1:β ^ 2 = 1⊢ False β:ℝhβ:-1 < β ∧ β < 1hn:1 - β ^ 2 = 0h1:β = 1 ∨ β = -1⊢ False All goals completed! 🐙

The Lorentz boost with in the space direction i with speed β with |β| < 1.

d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0hj':¬j = i⊢ ((if k = Sum.inl 0 then if Sum.inr j = Sum.inl 0 then -1 * γ β * γ β else if Sum.inr j = Sum.inr i then -(-1 * (γ β * β) * γ β) else if Sum.inl 0 = Sum.inr j then -1 * γ β else 0 else if k = Sum.inr i then -if Sum.inr j = Sum.inl 0 then -1 * γ β * (γ β * β) else if Sum.inr j = Sum.inr i then -(-1 * (γ β * β) * (γ β * β)) else if Sum.inl 0 = Sum.inr j then -1 * (γ β * β) else 0 else if Sum.inl 0 = k then if Sum.inr j = Sum.inl 0 then -1 * γ β else if Sum.inr j = Sum.inr i then -(-1 * (γ β * β)) else if Sum.inl 0 = Sum.inr j then -1 else 0 else 0) + if k = Sum.inl 0 ∧ j = i then -if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) * (γ β * β) else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β * (γ β * β)) else if Sum.inr j = Sum.inr j then -(-1 * (γ β * β)) else 0 else if k = Sum.inr i ∧ j = i then if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) * γ β else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β * γ β) else if Sum.inr j = Sum.inr j then -(-1 * γ β) else 0 else if Sum.inr j = k then if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β) else if Sum.inr j = Sum.inr j then - -1 else 0 else 0) = if Sum.inr j = k then 1 else 0 All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0⊢ ∀ b ∈ Finset.univ, b ≠ j → (if k = Sum.inl 0 ∧ b = i then -if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) * (γ β * β) else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β * (γ β * β)) else if Sum.inr b = Sum.inr j then -(-1 * (γ β * β)) else 0 else if k = Sum.inr i ∧ b = i then if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) * γ β else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β * γ β) else if Sum.inr b = Sum.inr j then -(-1 * γ β) else 0 else if Sum.inr b = k then if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β) else if Sum.inr b = Sum.inr j then - -1 else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ j⊢ (if k = Sum.inl 0 ∧ b = i then -if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) * (γ β * β) else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β * (γ β * β)) else if Sum.inr b = Sum.inr j then -(-1 * (γ β * β)) else 0 else if k = Sum.inr i ∧ b = i then if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) * γ β else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β * γ β) else if Sum.inr b = Sum.inr j then -(-1 * γ β) else 0 else if Sum.inr b = k then if Sum.inr j = Sum.inl 0 ∧ b = i then -1 * (γ β * β) else if Sum.inr j = Sum.inr i ∧ b = i then -(-1 * γ β) else if Sum.inr b = Sum.inr j then - -1 else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ j⊢ (if k = Sum.inl 0 ∧ b = i then -if j = i ∧ b = i then - -(γ β * (γ β * β)) else 0 else if k = Sum.inr i ∧ b = i then if j = i ∧ b = i then - -(γ β * γ β) else 0 else if Sum.inr b = k then if j = i ∧ b = i then - -γ β else 0 else 0) = 0 match k with d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ j⊢ (if Sum.inl 0 = Sum.inl 0 ∧ b = i then -if j = i ∧ b = i then - -(γ β * (γ β * β)) else 0 else if Sum.inl 0 = Sum.inr i ∧ b = i then if j = i ∧ b = i then - -(γ β * γ β) else 0 else if Sum.inr b = Sum.inl 0 then if j = i ∧ b = i then - -γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ j⊢ b = i → j = i → b = i → γ β = 0 ∨ β = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jh1:b = ih2:j = i⊢ b = i → γ β = 0 ∨ β = 0 d:ℕΛ:↑(𝓛 d)β:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0a✝:j ∈ Finset.univhb:j ≠ j⊢ j = j → γ β = 0 ∨ β = 0 All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin d⊢ (if Sum.inr k = Sum.inl 0 ∧ b = i then -if j = i ∧ b = i then - -(γ β * (γ β * β)) else 0 else if Sum.inr k = Sum.inr i ∧ b = i then if j = i ∧ b = i then - -(γ β * γ β) else 0 else if Sum.inr b = Sum.inr k then if j = i ∧ b = i then - -γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin d⊢ (if k = i ∧ b = i then if j = i ∧ b = i then γ β * γ β else 0 else if b = k then if j = i ∧ b = i then γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin dhb':b = i⊢ (if k = i ∧ b = i then if j = i ∧ b = i then γ β * γ β else 0 else if b = k then if j = i ∧ b = i then γ β else 0 else 0) = 0d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin dhb':¬b = i⊢ (if k = i ∧ b = i then if j = i ∧ b = i then γ β * γ β else 0 else if b = k then if j = i ∧ b = i then γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin dhb':b = i⊢ (if k = i ∧ b = i then if j = i ∧ b = i then γ β * γ β else 0 else if b = k then if j = i ∧ b = i then γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin dhb':b = i⊢ (if k = i then if j = i then γ β * γ β else 0 else if i = k then if j = i then γ β else 0 else 0) = 0 d:ℕΛ:↑(𝓛 d)β:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin d⊢ (if k = b then if j = b then γ β * γ β else 0 else if b = k then if j = b then γ β else 0 else 0) = 0 All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0b:Fin da✝:b ∈ Finset.univhb:b ≠ jk:Fin dhb':¬b = i⊢ (if k = i ∧ b = i then if j = i ∧ b = i then γ β * γ β else 0 else if b = k then if j = i ∧ b = i then γ β else 0 else 0) = 0 All goals completed! 🐙 d:ℕΛ:↑(𝓛 d)i:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dhγ:γ β ^ 2 - γ β ^ 2 * β ^ 2 = 1j:Fin dhj:¬Sum.inr j = Sum.inl 0⊢ j ∉ Finset.univ → (if k = Sum.inl 0 ∧ j = i then -if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) * (γ β * β) else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β * (γ β * β)) else if Sum.inr j = Sum.inr j then -(-1 * (γ β * β)) else 0 else if k = Sum.inr i ∧ j = i then if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) * γ β else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β * γ β) else if Sum.inr j = Sum.inr j then -(-1 * γ β) else 0 else if Sum.inr j = k then if Sum.inr j = Sum.inl 0 ∧ j = i then -1 * (γ β * β) else if Sum.inr j = Sum.inr i ∧ j = i then -(-1 * γ β) else if Sum.inr j = Sum.inr j then - -1 else 0 else 0) = 0 All goals completed! 🐙
@[simp] lemma boost_transpose_eq_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) : transpose (boost i β hβ) = boost i β hβ := d:ℕi:Fin dβ:ℝhβ:|β| < 1⊢ transpose (boost i β hβ) = boost i β hβ d:ℕi:Fin dβ:ℝhβ:|β| < 1j:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin d⊢ ↑(transpose (boost i β hβ)) j k = ↑(boost i β hβ) j k d:ℕi:Fin dβ:ℝhβ:|β| < 1j:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin d⊢ (if j = Sum.inl 0 ∧ k = Sum.inl 0 then γ β else if j = Sum.inl 0 ∧ k = Sum.inr i then -(γ β * β) else if j = Sum.inr i ∧ k = Sum.inl 0 then -(γ β * β) else if j = Sum.inr i ∧ k = Sum.inr i then γ β else if k = j then 1 else 0) = if k = Sum.inl 0 ∧ j = Sum.inl 0 then γ β else if k = Sum.inl 0 ∧ j = Sum.inr i then -(γ β * β) else if k = Sum.inr i ∧ j = Sum.inl 0 then -(γ β * β) else if k = Sum.inr i ∧ j = Sum.inr i then γ β else if j = k then 1 else 0 match j, k with d:ℕi:Fin dβ:ℝhβ:|β| < 1j:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin d⊢ (if Sum.inl 0 = Sum.inl 0 ∧ Sum.inl 0 = Sum.inl 0 then γ β else if Sum.inl 0 = Sum.inl 0 ∧ Sum.inl 0 = Sum.inr i then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inl 0 = Sum.inl 0 then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inl 0 = Sum.inr i then γ β else if Sum.inl 0 = Sum.inl 0 then 1 else 0) = if Sum.inl 0 = Sum.inl 0 ∧ Sum.inl 0 = Sum.inl 0 then γ β else if Sum.inl 0 = Sum.inl 0 ∧ Sum.inl 0 = Sum.inr i then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inl 0 = Sum.inl 0 then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inl 0 = Sum.inr i then γ β else if Sum.inl 0 = Sum.inl 0 then 1 else 0 All goals completed! 🐙 d:ℕi:Fin dβ:ℝhβ:|β| < 1j:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dk:Fin d⊢ (if Sum.inl 0 = Sum.inl 0 ∧ Sum.inr k = Sum.inl 0 then γ β else if Sum.inl 0 = Sum.inl 0 ∧ Sum.inr k = Sum.inr i then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inr k = Sum.inl 0 then -(γ β * β) else if Sum.inl 0 = Sum.inr i ∧ Sum.inr k = Sum.inr i then γ β else if Sum.inr k = Sum.inl 0 then 1 else 0) = if Sum.inr k = Sum.inl 0 ∧ Sum.inl 0 = Sum.inl 0 then γ β else if Sum.inr k = Sum.inl 0 ∧ Sum.inl 0 = Sum.inr i then -(γ β * β) else if Sum.inr k = Sum.inr i ∧ Sum.inl 0 = Sum.inl 0 then -(γ β * β) else if Sum.inr k = Sum.inr i ∧ Sum.inl 0 = Sum.inr i then γ β else if Sum.inl 0 = Sum.inr k then 1 else 0 All goals completed! 🐙 d:ℕi✝:Fin dβ:ℝhβ:|β| < 1j:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin di:Fin d⊢ (if Sum.inr i = Sum.inl 0 ∧ Sum.inl 0 = Sum.inl 0 then γ β else if Sum.inr i = Sum.inl 0 ∧ Sum.inl 0 = Sum.inr i✝ then -(γ β * β) else if Sum.inr i = Sum.inr i✝ ∧ Sum.inl 0 = Sum.inl 0 then -(γ β * β) else if Sum.inr i = Sum.inr i✝ ∧ Sum.inl 0 = Sum.inr i✝ then γ β else if Sum.inl 0 = Sum.inr i then 1 else 0) = if Sum.inl 0 = Sum.inl 0 ∧ Sum.inr i = Sum.inl 0 then γ β else if Sum.inl 0 = Sum.inl 0 ∧ Sum.inr i = Sum.inr i✝ then -(γ β * β) else if Sum.inl 0 = Sum.inr i✝ ∧ Sum.inr i = Sum.inl 0 then -(γ β * β) else if Sum.inl 0 = Sum.inr i✝ ∧ Sum.inr i = Sum.inr i✝ then γ β else if Sum.inr i = Sum.inl 0 then 1 else 0 All goals completed! 🐙 d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin d⊢ (if Sum.inr j = Sum.inl 0 ∧ Sum.inr k = Sum.inl 0 then γ β else if Sum.inr j = Sum.inl 0 ∧ Sum.inr k = Sum.inr i then -(γ β * β) else if Sum.inr j = Sum.inr i ∧ Sum.inr k = Sum.inl 0 then -(γ β * β) else if Sum.inr j = Sum.inr i ∧ Sum.inr k = Sum.inr i then γ β else if Sum.inr k = Sum.inr j then 1 else 0) = if Sum.inr k = Sum.inl 0 ∧ Sum.inr j = Sum.inl 0 then γ β else if Sum.inr k = Sum.inl 0 ∧ Sum.inr j = Sum.inr i then -(γ β * β) else if Sum.inr k = Sum.inr i ∧ Sum.inr j = Sum.inl 0 then -(γ β * β) else if Sum.inr k = Sum.inr i ∧ Sum.inr j = Sum.inr i then γ β else if Sum.inr j = Sum.inr k then 1 else 0 All goals completed! 🐙All goals completed! 🐙d:ℕi:Fin dj✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin d⊢ (if Sum.inr k = Sum.inl 0 ∧ Sum.inr j = Sum.inl 0 then γ 0 else if Sum.inr k = Sum.inl 0 ∧ Sum.inr j = Sum.inr i then 0 else if Sum.inr k = Sum.inr i ∧ Sum.inr j = Sum.inl 0 then 0 else if Sum.inr k = Sum.inr i ∧ Sum.inr j = Sum.inr i then γ 0 else if Sum.inr j = Sum.inr k then 1 else 0) = if Sum.inr j = Sum.inr k then 1 else 0 d:ℕi:Fin dj✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin d⊢ k = i → j = i → γ 0 = if j = k then 1 else 0 d:ℕi:Fin dj✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh1:k = ih2:j = i⊢ γ 0 = if j = k then 1 else 0 d:ℕj✝:Fin 1 ⊕ Fin dk:Fin 1 ⊕ Fin dj:Fin d⊢ γ 0 = if j = j then 1 else 0 All goals completed! 🐙d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin d⊢ -1 * ↑(boost i β hβ) (Sum.inr k) (Sum.inr j) * -1 = ↑(boost i (-β) ⋯) (Sum.inr j) (Sum.inr k) d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin d⊢ (-if j = i ∧ k = i then -γ β else if j = k then -1 else 0) = if j = i ∧ k = i then γ β else if j = k then 1 else 0 d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝:j = i ∧ k = i⊢ - -γ β = γ βd:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝:¬(j = i ∧ k = i)⊢ (-if j = k then -1 else 0) = if j = k then 1 else 0 <;> [d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝:j = i ∧ k = i⊢ - -γ β = γ β; d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝¹:¬(j = i ∧ k = i)h✝:j = k⊢ - -1 = 1d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝¹:¬(j = i ∧ k = i)h✝:¬j = k⊢ -0 = 0] d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝:j = i ∧ k = i⊢ - -γ β = γ βd:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝¹:¬(j = i ∧ k = i)h✝:j = k⊢ - -1 = 1d:ℕi:Fin dβ:ℝhβ:|β| < 1j✝:Fin 1 ⊕ Fin dk✝:Fin 1 ⊕ Fin dj:Fin dk:Fin dh✝¹:¬(j = i ∧ k = i)h✝:¬j = k⊢ -0 = 0 All goals completed! 🐙@[simp] lemma boost_inl_0_inl_0 (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (boost i β hβ).1 (Sum.inl 0) (Sum.inl 0) = γ β := d:ℕi:Fin dβ:ℝhβ:|β| < 1⊢ ↑(boost i β hβ) (Sum.inl 0) (Sum.inl 0) = γ β All goals completed! 🐙@[simp] lemma boost_inr_self_inr_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (boost i β hβ).1 (Sum.inr i) (Sum.inr i) = γ β := d:ℕi:Fin dβ:ℝhβ:|β| < 1⊢ ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) = γ β All goals completed! 🐙@[simp] lemma boost_inl_0_inr_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (boost i β hβ).1 (Sum.inl 0) (Sum.inr i) = - γ β * β := d:ℕi:Fin dβ:ℝhβ:|β| < 1⊢ ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) = -γ β * β All goals completed! 🐙@[simp] lemma boost_inr_self_inl_0 (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (boost i β hβ).1 (Sum.inr i) (Sum.inl 0) = - γ β * β := d:ℕi:Fin dβ:ℝhβ:|β| < 1⊢ ↑(boost i β hβ) (Sum.inr i) (Sum.inl 0) = -γ β * β All goals completed! 🐙lemma boost_inl_0_inr_other {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) : (boost i β hβ).1 (Sum.inl 0) (Sum.inr j) = 0 := d:ℕi:Fin dj:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ ↑(boost i β hβ) (Sum.inl 0) (Sum.inr j) = 0 All goals completed! 🐙lemma boost_inr_other_inl_0 {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) : (boost i β hβ).1 (Sum.inr j) (Sum.inl 0) = 0 := d:ℕi:Fin dj:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ ↑(boost i β hβ) (Sum.inr j) (Sum.inl 0) = 0 All goals completed! 🐙lemma boost_inr_self_inr_other {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) : (boost i β hβ).1 (Sum.inr i) (Sum.inr j) = 0 := d:ℕi:Fin dj:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ ↑(boost i β hβ) (Sum.inr i) (Sum.inr j) = 0 All goals completed! 🐙lemma boost_inr_other_inr_self {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) : (boost i β hβ).1 (Sum.inr j) (Sum.inr i) = 0 := d:ℕi:Fin dj:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ ↑(boost i β hβ) (Sum.inr j) (Sum.inr i) = 0 All goals completed! 🐙lemma boost_inr_other_inr {i j k : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) : (boost i β hβ).1 (Sum.inr j) (Sum.inr k) = if j = k then 1 else 0:= d:ℕi:Fin dj:Fin dk:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ ↑(boost i β hβ) (Sum.inr j) (Sum.inr k) = if j = k then 1 else 0 All goals completed! 🐙d:ℕi:Fin dj:Fin dk:Fin dβ:ℝhβ:|β| < 1hij:j ≠ i⊢ j ≠ i All goals completed! 🐙

Properties of boosts in the zero-direction

@[simp] lemma boost_zero_inl_0_inr_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inl 0) (Sum.inr i.succ) = 0 := boost_inl_0_inr_other hβ (Fin.succ_ne_zero i)@[simp] lemma boost_zero_inr_succ_inl_0{d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr i.succ) (Sum.inl 0) = 0 := boost_inr_other_inl_0 hβ (Fin.succ_ne_zero i)@[simp] lemma boost_zero_inl_0_inr_nat_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inl 0) (Sum.inr ⟨i + 1, h⟩) = 0 := boost_inl_0_inr_other hβ (Fin.ne_of_val_ne (Nat.succ_ne_zero i))@[simp] lemma boost_zero_inr_nat_succ_inl_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr ⟨i + 1, h⟩) (Sum.inl 0) = 0 := boost_inr_other_inl_0 hβ (Fin.ne_of_val_ne (Nat.succ_ne_zero i))@[simp] lemma boost_zero_inr_0_inr_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr 0) (Sum.inr i.succ) = 0 := boost_inr_self_inr_other hβ (Fin.succ_ne_zero i)@[simp] lemma boost_zero_inr_succ_inr_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr i.succ) (Sum.inr 0) = 0 := boost_inr_other_inr_self hβ (Fin.succ_ne_zero i)@[simp] lemma boost_zero_inr_0_inr_nat_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr 0) (Sum.inr ⟨i + 1, h⟩) = 0 := boost_inr_self_inr_other hβ (Fin.ne_of_val_ne (Nat.succ_ne_zero i))@[simp] lemma boost_zero_inr_nat_succ_inr_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) : (boost (0 : Fin d.succ) β hβ).1 (Sum.inr ⟨i + 1, h⟩) (Sum.inr 0) = 0 := boost_inr_other_inr_self hβ (Fin.ne_of_val_ne (Nat.succ_ne_zero i))d:ℕβ:ℝhβ:|β| < 1i1:Fin di2:Fin d⊢ (if i2.succ = i1.succ then 1 else 0) = if i1 = i2 then 1 else 0 All goals completed! 🐙