ScheduledCopiedSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prime support of the actual copied assignment

theorem OAI.Ostmann.retainedPairwise_parts line 13

Source documentation

The retained tuple has separate H and Y support and coprime total products.

theorem retainedPairwise_parts {H Y : Type*} [Fintype H] [Fintype Y]
    (L : H → ℕ) (U : Y → ℕ)
    (h : Pairwise (fun i j => (Sum.elim L U i).Coprime (Sum.elim L U j))) :
    Pairwise (fun i j => (L i).Coprime (L j)) ∧
      Pairwise (fun i j => (U i).Coprime (U j)) ∧
      (∏ i, L i).Coprime (∏ j, U j) := by
…

theorem OAI.Ostmann.scheduledCopiedAssignment_pairwise_branch line 32

Source documentation

Restricting a pairwise copied assignment to either retained branch recovers its full H/Y coprimality, including cross terms.

theorem scheduledCopiedAssignment_pairwise_branch {I : Type*}
    (role : I → CopyScheduleRole) (n : ℕ)
    (L R : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
    (h : Pairwise (fun i j =>
      (scheduledCopiedAssignment role n U L R i).Coprime
        (scheduledCopiedAssignment role n U L R j))) (b : Bool) :
    Pairwise (fun i j =>
      (Sum.elim (if b then L else R) U i).Coprime (Sum.elim (if b then L else R) U j)) := by
…

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

theorem OAI.Ostmann.scheduledCopiedAssignment_support line 70

Source documentation

Signed reconstruction, the original branch support and the prime cutoff supply every prime-level test on the next copied assignment.

theorem scheduledCopiedAssignment_support {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (n : ℕ)
    (L R : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
    [∀ h, Fact (L h).Prime] [∀ h, Fact (R h).Prime] [∀ y, Fact (U y).Prime]
    (M B K V : ℕ) (v w s : ℤ) (hMpos : 0 < M) (hs : s ≠ 0)
    (hrel : v * (∏ h, R h) - w * (∏ h, L h) = s * M)
    (hv : v.natAbs ≤ B) (hw : w.natAbs ≤ B)
    (hLbound : (∏ h, L h) ≤ K) (hRbound : (∏ h, R h) ≤ K)
    (hscale : 2 * B * K ≤ V * M)
    (hL : Pairwise (fun i j => (Sum.elim L U i).Coprime (Sum.elim L U j)))
    (hR : Pairwise (fun i j => (Sum.elim R U i).Coprime (Sum.elim R U j)))
    (hML : M.Coprime ((∏ h, L h) * ∏ y, U y))
…

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