RepeatedPivotPhase.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Repeated prime constituents of the current pivot vanish identically

theorem OAI.Ostmann.directedPrimePhase_eq_zero_of_edge line 11

theorem OAI.Ostmann.sampledScheduledPhase_eq_zero_of_repeat line 26

Source documentation

Restricting the current pivot tuple to distinct primes loses no amplitude: its regular row already kills every repeated tuple.

theorem sampledScheduledPhase_eq_zero_of_repeat {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : I → ℕ → ℂ) (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n) (t : FrequencyTree ℤ n)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (x : Fin r → P)
    (L : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
    [∀ h, Fact (L h).Prime] [∀ y, Fact (U y).Prime]
    (center : ∀ p : ℕ, ZMod p) (i j : Fin r) (hij : i ≠ j) (hrep : x i = x j) :
    sampledScheduledPhase role χ κ pivot n r e t P hP x L U center = 0 := by
…

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

theorem OAI.Ostmann.sampledScheduledPhase_eq_zero_of_not_injective line 49

theorem OAI.Ostmann.scheduledCurrentAmplitude_restrict_injective line 63

Source documentation

The tuple set required by the factorial Cauchy bound is obtained exactly; there is no repeated-prime loss at a pivot elimination.

theorem scheduledCurrentAmplitude_restrict_injective {I A Z : Type*}
    [Fintype I] [Fintype A] [Fintype Z]
    (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : I → ℕ → ℂ) (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n) (hist : A → FrequencyTree ℤ n)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : Fin r → Finset ℕ)
    (L : A → CopyScheduleH role n → ℕ) (U : Z → CopyScheduleY role n → ℕ)
    [∀ a h, Fact (L a h).Prime] [∀ z y, Fact (U z y).Prime]
    (center : ∀ p : ℕ, ZMod p) (W : Z → ℕ → A → ℂ) (μ : Z → ℝ) :
    scheduledCurrentAmplitude role χ κ pivot n r e hist P hP Q Finset.univ L U center W μ =
      scheduledCurrentAmplitude role χ κ pivot n r e hist P hP Q
        (Finset.univ.filter Function.Injective) L U center W μ := by
…

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