X Variable Properties

In this file we introduce some generally helpful lemmas for X as introduced in Elligator.Elligator1.Variables.

References

See [bernstein2013a], Section 3.2, Theorem 1.

theorem Elligator.Elligator1.X_pow_two_add_one_div_c_pow_two_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : X t s ^ 2 + 1 / c s ^ 2 ≠ 0

theorem Elligator.Elligator1.X_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : X t s ≠ 0

theorem Elligator.Elligator1.X_comparison {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have X1 := X t s; have X2 := X ⟨t2, ⋯⟩ s; X2 = 1 / X1

@[simp]

theorem Elligator.Elligator1.X_of_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have X0 := X ⟨0, ⋯⟩ s; X0 = 1