OAI/NumberTheory/Ostmann/Construction/ScheduledCopiedAmplitude.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledNextAmplitude line 14

   Source documentation

   The two old frequency histories become the two children of the new root. Only the forced positive integer pivot is inserted into the inherited weights.

   noncomputable def scheduledNextAmplitude {I A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (g : I → I → ℤ) (pivot : ℕ → I) (initial : I → ℤ → ℕ → ℂ)
       (n : ℕ) (hist : A → FrequencyTree ℤ n)
       (L : A → CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
       [∀ a h, Fact (L a h).Prime] [∀ y, Fact (U y).Prime]
       (center : ∀ p : ℕ, ZMod p) (W : ℕ → A → ℂ) (T : Finset ℕ) (V : ℕ) : ℂ :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY

2. theorem OAI.Ostmann.copiedWeightedAmplitude_eq_scheduledNextAmplitude line 32
3. theorem OAI.Ostmann.reconstructedOffDiagonal_eq_scheduledNextAmplitude line 61

   Source documentation

   The equality carries every inherited weight and every integer-pivot test. Its support assumptions are only the original branch assumptions.

   theorem reconstructedOffDiagonal_eq_scheduledNextAmplitude {I A : Type*}
       [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (g : I → I → ℤ) (pivot : ℕ → I) (initial : I → ℤ → ℕ → ℂ)
       (n : ℕ) (hist : A → FrequencyTree ℤ n)
       (L : A → CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
       [∀ a h, Fact (L a h).Prime] [∀ y, Fact (U y).Prime]
       (center : ∀ p : ℕ, ZMod p) (W : ℕ → A → ℂ) (T : Finset ℕ) (B K V : ℕ)
       (hT : ∀ M ∈ T, 0 < M)
       (hsupport : ∀ M ∈ T, ∀ a, W M a ≠ 0 →
         Pairwise (fun i j => (Sum.elim (L a) U i).Coprime (Sum.elim (L a) U j)) ∧
         M.Coprime ((∏ h, L a h) * ∏ y, U y) ∧
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY