OAI/NumberTheory/Ostmann/Construction/MatchedRetainedPhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.retainedInternalGraph line 12
2. def OAI.Ostmann.externalPivotUnary line 15
3. def OAI.Ostmann.externalPivotCenter line 21
4. theorem OAI.Ostmann.externalPivotUnary_norm_le_one line 24
5. theorem OAI.Ostmann.retainedGroupedPhase_eq_directed line 35

   Source documentation

   At a fixed external pivot, both the translating center and the extra incoming character power depend only on the actual prime.

   theorem retainedGroupedPhase_eq_directed {I : Type*} [Fintype I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime]
       (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (t : ∀ p : ℕ, ZMod p) (ν : I → ℕ → ℂ)
       (b : Option I → Option I → ℤ) (M : ℕ) (v : ℤ) :
       retainedGroupedPhase p (fun i => χ i (p i)) (fun i => t (p i))
           (fun i => ν i (p i)) b M v =
         directedPrimePhase p (fun i => χ i (p i)) (fun i => externalPivotCenter M t (p i))
           (fun i => externalPivotUnary χ b ν M i (p i)) (retainedInternalGraph b) v := by
   …

   Mentions: OAI.Ostmann.retainedGroupedPhase, OAI.Ostmann.directedPrimePhase, OAI.Ostmann.externalPivotCenter, OAI.Ostmann.externalPivotUnary, OAI.Ostmann.retainedInternalGraph

6. theorem OAI.Ostmann.matched_retained_phase_quotient line 57

   Source documentation

   The additive factors cancel on the diagonal with the external pivot fixed. Its incoming character powers remain exactly in the unary factors.

   theorem matched_retained_phase_quotient {I J : Type*} [Fintype I] [Fintype J]
       (e : I ≃ J) (χ : J → ∀ p : ℕ, DirichletCharacter ℂ p)
       (p : J → ℕ) [∀ j, Fact (p j).Prime] (t : ∀ p : ℕ, ZMod p)
       (ν : I → ℕ → ℂ) (ω : J → ℕ → ℂ)
       (b : Option I → Option I → ℤ) (c : Option J → Option J → ℤ) (M : ℕ) (v : ℤ)
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (hb : ∀ i, b (some i) (some i) = 0) (hcdiag : ∀ j, c (some j) (some j) = 0) :
       retainedGroupedPhase (fun i => p (e i)) (fun i => χ (e i) (p (e i)))
           (fun i => t (p (e i))) (fun i => ν i (p (e i))) b M v *
         conj (retainedGroupedPhase p (fun j => χ j (p j)) (fun j => t (p j))
           (fun j => ω j (p j)) c M v) =
         finiteEdgeWeight
   …

   Mentions: OAI.Ostmann.retainedGroupedPhase, OAI.Ostmann.finiteEdgeWeight