TransferRowProducts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Complete local rows and their product under transfer

theorem OAI.Ostmann.transfer_left_row line 14

Source documentation

The incoming pivot column becomes one constant exponent on every opposite-branch constituent. The other old row factors are retained.

theorem transfer_left_row {I : Type*} [Fintype I] {p : ℕ} [Fact p.Prime]
    (χ : DirichletCharacter ℂ p) (P D v s t : ZMod p) (R : I → ZMod p)
    (ν S O : ℂ) (b : ℤ)
    (hP : P ≠ 0) (hD : D ≠ 0) (hR : (∏ i, R i) ≠ 0) (hs : s ≠ 0)
    (hrel : v * (∏ i, R i) = s * P) :
    ZMod.stdAddChar (t * (v / (P * D))) * ν * χ P ^ b * S * O =
      ZMod.stdAddChar (t * (s / ((∏ i, R i) * D))) *
        (ν * χ (v / s) ^ b) * S * (∏ i, χ (R i) ^ b) * O := by
…

theorem OAI.Ostmann.transfer_right_row line 29

Source documentation

The conjugated right row has the negative incoming exponent on every left-branch constituent. This includes its new unary factor exactly.

theorem transfer_right_row {I : Type*} [Fintype I] {p : ℕ} [Fact p.Prime]
    (χ : DirichletCharacter ℂ p) (P D w s t : ZMod p) (L : I → ZMod p)
    (ν S O : ℂ) (b : ℤ)
    (hP : P ≠ 0) (hD : D ≠ 0) (hL : (∏ i, L i) ≠ 0) (hs : s ≠ 0)
    (hrel : -w * (∏ i, L i) = s * P) :
    conj (ZMod.stdAddChar (t * (w / (P * D))) * ν * χ P ^ b * S * O) =
      ZMod.stdAddChar (t * (s / ((∏ i, L i) * D))) *
        (conj ν * χ (-w / s) ^ (-b)) * conj S * (∏ i, χ (L i) ^ (-b)) * conj O := by
…

theorem OAI.Ostmann.transfer_outside_row line 46

Source documentation

Every common outside factor cancels at a shared slot. The remaining incoming exponents on the copied branches have opposite signs.

theorem transfer_outside_row {p : ℕ} [Fact p.Prime]
    (P L R D v w s t : ZMod p) (νv νw C SL SR : ℂ)
    (hP : P ≠ 0) (hL : L ≠ 0) (hR : R ≠ 0) (hD : D ≠ 0)
    (hC : ‖C‖ = 1) (hrel : v * R - w * L = s * P) :
    (ZMod.stdAddChar (t * (v / (P * L * D))) * νv * C * SL) *
      conj (ZMod.stdAddChar (t * (w / (P * R * D))) * νw * C * SR) =
    ZMod.stdAddChar (t * (s / (L * R * D))) * (νv * conj νw) * SL * conj SR := by
…

theorem OAI.Ostmann.character_row_norm_one line 66
Source documentation
Products of actual unit character factors have unit modulus, for all integer exponents. This discharges the common-row cancellation hypothesis.
```
theorem character_row_norm_one {I : Type*} [Fintype I] {p : ℕ}
    (χ : DirichletCharacter ℂ p) (q : I → ZMod p) (b : I → ℤ)
    (hq : ∀ i, IsUnit (q i)) : ‖∏ i, χ (q i) ^ b i‖ = 1 := by
…
```

theorem OAI.Ostmann.transfer_phase_product line 77

Source documentation

Left and right rows separate, while each shared outside row is paired before its product is taken.

theorem transfer_phase_product {H Y : Type*} [Fintype H] [Fintype Y]
    (left right : H → ℂ) (outLeft outRight : Y → ℂ) :
    ((∏ h, left h) * ∏ y, outLeft y) * conj ((∏ h, right h) * ∏ y, outRight y) =
      (∏ h, left h) * (∏ h, conj (right h)) * ∏ y, outLeft y * conj (outRight y) := by
…