RowBound on the index types Fin n

RowBound quantifies over all finite index types ι : Type; Theorem 1.7 of arXiv:2410.19062 is about [n]. The statement restricted to the index types Fin n (RowBoundFin) already implies RowBound (transport along Fintype.equivFin). So the generality of RowBound in the index type asks for nothing beyond the [n] statement (rowBound_iff_fin).

def AaronsonAmbainis.Bridge.RowBoundFin : Prop

RowBound, restricted to the index types Fin n.

Equations

• One or more equations did not get rendered due to their size.

theorem AaronsonAmbainis.Bridge.chi_comp_equiv {ι : Type u_1} {κ : Type u_2} (e : ι ≃ κ) (S : Finset ι) (y : Cube κ) : (chi S fun (i : ι) => y (e i)) = chi (Finset.map e.toEmbedding S) y

theorem AaronsonAmbainis.Bridge.hasDegreeLE_comp_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) {f : Cube ι → ℝ} {d : ℕ} (h : HasDegreeLE f d) : HasDegreeLE (fun (y : Cube κ) => f fun (i : ι) => y (e i)) d

HasDegreeLE is invariant under relabelling the coordinates.

theorem AaronsonAmbainis.Bridge.diffSet_comp_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (x y : Cube ι) : (diffSet (fun (k : κ) => x (e.symm k)) fun (k : κ) => y (e.symm k)) = Finset.map e.toEmbedding (diffSet x y)

theorem AaronsonAmbainis.Bridge.rowBound_concl_transport {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (f : Cube ι → ℝ) (B : ℝ) (h : ∃ (c : Cube κ → κ → ℝ), (∀ (x y : Cube κ), |(f fun (i : ι) => x (e i)) - f fun (i : ι) => y (e i)| ≤ ∑ k ∈ diffSet x y, c x k) ∧ ∀ (x : Cube κ), ∑ k : κ, c x k ≤ B) : ∃ (c : Cube ι → ι → ℝ), (∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, c x i) ∧ ∀ (x : Cube ι), ∑ i : ι, c x i ≤ B

The conclusion of RowBound transports along an equivalence of index types.

theorem AaronsonAmbainis.Bridge.rowBound_of_fin (h : RowBoundFin) : RowBound

The [n] statement implies the statement for all finite index types.

theorem AaronsonAmbainis.Bridge.rowBoundFin_of_rowBound (h : RowBound) : RowBoundFin

theorem AaronsonAmbainis.Bridge.rowBound_iff_fin : RowBound ↔ RowBoundFin

RowBound is equivalent to its restriction to the index types Fin n.