OAI/NumberTheory/Ostmann/Tree/PairOrientationValue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.fieldBottomPairValue_formula line 11
2. theorem OAI.Ostmann.fieldBottomPairValue_reverse line 23

   Source documentation

   Reversing a pair negates its difference, inverts its ratio and conjugates its base function. The two leaf factors themselves remain unchanged.

   theorem fieldBottomPairValue_reverse {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (d t : ZMod p) :
       fieldBottomPairValue (fun x => conj (g x)) (-d) t⁻¹ = fieldBottomPairValue g d t := by
   …

   Mentions: OAI.Ostmann.fieldBottomPairValue

3. theorem OAI.Ostmann.fieldBottomPairValue_negate line 45
4. theorem OAI.Ostmann.fieldBottomPairValue_reflect_reverse line 60

   Source documentation

   Reversing the pair while keeping its difference positive reflects and conjugates the base function.

   theorem fieldBottomPairValue_reflect_reverse {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (d t : ZMod p) :
       fieldBottomPairValue (fun x => conj (g (-x))) d t⁻¹ = fieldBottomPairValue g d t := by
   …

   Mentions: OAI.Ostmann.fieldBottomPairValue