OAI/Computability/FourierCircuit/FiniteSeparation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Packing.finite_separator line 11

    Source documentation

    Finite comparison alternative, exactly the separator needed for no-win prices.

    theorem finite_separator {ρ τ : Type} [Fintype ρ] [Fintype τ] [Nonempty τ]
 (Δ : ρ→τ→ℝ)
 (hn : ¬∃ lam : ρ→ℝ,(∀ r,0≤lam r) ∧ ∀ t,0<∑ r,lam r*Δ r t) :
 ∃ v : τ→ℝ,(∀ t,0≤v t) ∧ (∃ t,0<v t) ∧ ∀ r,∑ t,v t*Δ r t≤0 := by
…
  2. theorem OAI.ExactFourier.Packing.no_win_separator line 113
  3. theorem OAI.ExactFourier.Packing.finite_prices line 123
  4. theorem OAI.ExactFourier.Packing.finite_global_prices line 163
  5. theorem OAI.ExactFourier.Packing.global_prices_exist line 210
  6. theorem OAI.ExactFourier.Packing.GlobalConstraints.reindex_le line 234
  7. theorem OAI.ExactFourier.Packing.GlobalConstraints.reindex line 249
  8. def OAI.ExactFourier.Packing.GMatrix.of line 264
  9. def OAI.ExactFourier.Packing.rawValue line 267
  10. theorem OAI.ExactFourier.Packing.rawValue_unit line 271
  11. structure OAI.ExactFourier.Packing.RawPrice line 275
  12. theorem OAI.ExactFourier.Packing.rawPrice_exists line 285
  13. theorem OAI.ExactFourier.Embedded.matrix_inl line 315
  14. theorem OAI.ExactFourier.Embedded.matrix_inr line 327
  15. theorem OAI.ExactFourier.Embedded.matrix_refl line 339
  16. def OAI.ExactFourier.Packing.Word.sum line 347
  17. theorem OAI.ExactFourier.Packing.Word.matrix_sum line 349
  18. theorem OAI.ExactFourier.Packing.Word.weight_sum line 353
  19. theorem OAI.ExactFourier.Packing.Word.weight_kronecker line 357