OAI/Analysis/Littlewood/IntervalPacking.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.scaled_slot_conditions line 11
  2. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.choose_matching_loss line 37
  3. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.integer_slot_matching line 50
  4. def OAI.AsymptoticallyMinimalLittlewood.Packing.circleInterval line 146
  5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.circleInterval_disjoint_of_lifts line 149
  6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slots_separated line 168
  7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.actual_centers_separated line 188
  8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.siteCenter_margin line 207
  9. def OAI.AsymptoticallyMinimalLittlewood.Packing.signedLift line 225
  10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.signedLift_abs line 227
  11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.signedLift_separation line 229
  12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.circle_slots_disjoint line 243
  13. def OAI.AsymptoticallyMinimalLittlewood.Packing.signedCircle line 294
  14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.zmod_dot_circle line 296
  15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.signedSite_circle line 301
  16. theorem OAI.AsymptoticallyMinimalLittlewood.Packing.signed_interval_packing line 307
  17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.signed_interval_packing_fintype line 386
  18. theorem OAI.AsymptoticallyMinimalLittlewood.Packing.signed_interval_packing_general line 426

    Source documentation

    The minor degenerate-cardinality case is absorbed by a zero-coefficient fresh frequency. Only geometry is padded; the auxiliary polynomial is unchanged.

    theorem signed_interval_packing_general {I J : Type} [Fintype I] [Fintype J]
    [Nonempty I] (a : I → J → ℤ) (ha : ∀ i, a i≠0)
    (hnp : ∀ i j, i≠j → ∀ c : ℝ, ¬∀ k, (a j k : ℝ)=c*(a i k : ℝ))
    (w : I → ℝ) (hw : ∀ i, 0<w i) (hs : 2*∑ i, w i<1) :
    ∃ H : ℕ, 1≤H ∧ ∃ θ : Fin H → J → UnitAddCircle,
      ∀ e f : Bool, ∀ i j : I, ∀ h v : Fin H, (e,i,h)≠(f,j,v) →
        Disjoint (circleInterval (signedCircle e (∑ k, a i k • θ h k)) (w i/H))
          (circleInterval (signedCircle f (∑ k, a j k • θ v k)) (w j/H)) := by
…

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.circleInterval, OAI.AsymptoticallyMinimalLittlewood.Packing.signedCircle