OAI/Computability/FourierCircuit/InventoryValidity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExactFourier.Packing.inventory_card line 12
2. theorem OAI.ExactFourier.Packing.inventory_unit line 22
3. theorem OAI.ExactFourier.Packing.inventory_not_monomial line 28
4. theorem OAI.ExactFourier.Packing.exists_positive_dummy line 42
5. theorem OAI.ExactFourier.Packing.scalable_square_win line 86
6. theorem OAI.ExactFourier.Packing.integral_positive_combination line 206

   Source documentation

   Strict comparison positivity is preserved by sufficiently fine downward rational rounding.

   theorem integral_positive_combination {ρ τ : Type} [Fintype ρ] [Fintype τ]
    (Δ : ρ→τ→ℤ) (lam : ρ→ℝ) (hlam : ∀ r,0≤lam r)
    (hpos : ∀ t,0<∑ r,lam r*(Δ r t : ℝ)) :
    ∃ l : ρ→ℕ,∀ t,0<∑ r,(l r : ℤ)*Δ r t := by
   …

7. theorem OAI.ExactFourier.Packing.integer_comparison_win line 260
8. theorem OAI.ExactFourier.Packing.positive_comparison_win line 357