Exact Fourier circuits: inventory validity #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/InventoryValidity.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.
theorem
Complexity.ExactFourier.Packing.inventory_unit
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(hA : ∀ (t : τ), IsUnit (A t))
(k : τ → ℕ)
(I : ℕ)
:
theorem
Complexity.ExactFourier.Packing.inventory_not_monomial
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(hA : ∀ (t : τ), IsUnit (A t))
(k : τ → ℕ)
(I : ℕ)
(t : τ)
(hk : 0 < k t)
(hn : ¬MonomialMatrix (A t))
:
theorem
Complexity.ExactFourier.Packing.exists_positive_dummy
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(hA : ∀ (t : τ), IsUnit (A t))
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.scalable_square_win
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
[DecidableEq π]
(hA : ∀ (t : τ), IsUnit (A t))
(k : τ → ℕ)
(I : ℕ)
(hk : ∀ (t : τ), 0 < k t)
(anchor : τ)
(hn : ¬MonomialMatrix (A anchor))
(key : π → LivePair τ)
(P : (p : π) → FramedWord D (PairDomain D (key p)))
(m : π → ℕ)
(hP : ∀ (p : π), (P p).matrix = pairMatrix (key p))
(hnum :
∀ (s : LivePair τ), (∑ p : π, if key p = s then m p else 0) = speciesCopies k I (↑s).1 * speciesCopies k I (↑s).2)
(dummy : (t : τ) → FramedWord D (D t))
(hdpos : ∀ (t : τ), 0 < (dummy t).frames.length)
(hdummy : ∀ (t : τ), (dummy t).matrix = 1)
(hdtype : ∀ (t : τ) (o : Fin (dummy t).frames.length), ((dummy t).frames.get o).type = t)
(S : τ → ℕ)
(hS : ∀ (t : τ), 2 * k t ≤ S t)
(hGS : ∀ (t : τ), ∑ p : π, m p * List.count t (P p).types + S t = 2 * k t * (∑ i : τ, k i * Fintype.card (D i) + I))
(hdK : ∀ (t : τ), (dummy t).frames.length ∣ k t)
(hdS : ∀ (t : τ), (dummy t).frames.length ∣ S t)
(hreservoir : (2 * ∑ t : τ, k t * Fintype.card (D t)) * (∑ t : τ, k t * Fintype.card (D t) + I) ≤ I ^ 2)
:
theorem
Complexity.ExactFourier.Packing.integral_positive_combination
{ρ τ : Type}
[Fintype ρ]
[Fintype τ]
(Δ : ρ → τ → ℤ)
(lam : ρ → ℝ)
(hlam : ∀ (r : ρ), 0 ≤ lam r)
(hpos : ∀ (t : τ), 0 < ∑ r : ρ, lam r * ↑(Δ r t))
:
Strict comparison positivity is preserved by sufficiently fine downward rational rounding.
theorem
Complexity.ExactFourier.Packing.integer_comparison_win
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
[DecidableEq ρ]
(hA : ∀ (t : τ), IsUnit (A t))
(anchor : τ)
(hn : ¬MonomialMatrix (A anchor))
(c : ρ → PairComparison)
(l : ρ → ℕ)
(hpos : ∀ (t : τ), 0 < ∑ r : ρ, ↑(l r) * (c r).delta t)
:
theorem
Complexity.ExactFourier.Packing.positive_comparison_win
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
[DecidableEq ρ]
(hA : ∀ (t : τ), IsUnit (A t))
(anchor : τ)
(hn : ¬MonomialMatrix (A anchor))
(c : ρ → PairComparison)
(lam : ρ → ℝ)
(hlam : ∀ (r : ρ), 0 ≤ lam r)
(hpos : ∀ (t : τ), 0 < ∑ r : ρ, lam r * ↑((c r).delta t))
: