Rounding.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AsymptoticallyMinimalLittlewood.boolSign line 13
Source documentation
A Boolean encoding of a real sign.
```
def boolSign (b : Bool) : ℝ := if b then 1 else -1
```
theorem OAI.AsymptoticallyMinimalLittlewood.abs_boolSign line 15
theorem OAI.AsymptoticallyMinimalLittlewood.bool_exp_sum_le line 19
Source documentation
Elementary Rademacher MGF bound for one bounded coefficient.
```
theorem bool_exp_sum_le {a : ℝ} (ha : |a| ≤ 1) (t : ℝ) :
    (∑ b : Bool, Real.exp (t * a * boolSign b)) ≤ 2 * Real.exp (t ^ 2 / 2) := by
…
```
Mentions: OAI.AsymptoticallyMinimalLittlewood.boolSign

theorem OAI.AsymptoticallyMinimalLittlewood.signing_exp_sum_le line 35

Source documentation

MGF bound for all signings of a bounded real row, with counting measure.

theorem signing_exp_sum_le {α : Type u} [Fintype α] [DecidableEq α] (a : α → ℝ)
    (ha : ∀ k, |a k| ≤ 1) (t : ℝ) :
    (∑ x : α → Bool, Real.exp (t * ∑ k, a k * boolSign (x k))) ≤
      2 ^ Fintype.card α * Real.exp (t ^ 2 * Fintype.card α / 2) := by
…

Mentions: OAI.AsymptoticallyMinimalLittlewood.boolSign

theorem OAI.AsymptoticallyMinimalLittlewood.round_abs_le_exp_pair line 62

Source documentation

A pointwise bound for the cost of quantizing a row sum.

theorem round_abs_le_exp_pair {x d t : ℝ} (hd : 0 < d) (ht : 0 ≤ t)
    (htd : 4 ≤ t * d) :
    |(round (x / d) : ℝ)| ≤
      Real.exp (t * x - t * d / 4) + Real.exp (-t * x - t * d / 4) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.signing_round_sum_le line 102

Source documentation

Counting-measure bound for the average quantization cost of a bounded row.

theorem signing_round_sum_le {α : Type u} [Fintype α] [DecidableEq α] (a : α → ℝ)
    (ha : ∀ k, |a k| ≤ 1) {d t : ℝ} (hd : 0 < d) (ht : 0 ≤ t)
    (htd : 4 ≤ t * d) :
    (∑ x : α → Bool, |(round ((∑ k, a k * boolSign (x k)) / d) : ℝ)|) ≤
      2 ^ Fintype.card α * (2 * Real.exp (t ^ 2 * Fintype.card α / 2 - t * d / 4)) := by
…

Mentions: OAI.AsymptoticallyMinimalLittlewood.boolSign

theorem OAI.AsymptoticallyMinimalLittlewood.int_geometric_sum_le line 130
Source documentation
The geometric partition function for integer quantization labels.
```
theorem int_geometric_sum_le (S : Finset ℤ) {q : ℝ} (hq : 0 ≤ q) (hq' : q ≤ 1 / 2) :
    (∑ z ∈ S, q ^ z.natAbs) ≤ Real.exp (4 * q) := by
…
```

theorem OAI.AsymptoticallyMinimalLittlewood.int_exp_sum_le line 156

Source documentation

Each integer code has exponentially decaying weight.

theorem int_exp_sum_le (S : Finset ℤ) (a : ℝ) (ha : Real.exp (-a) ≤ 1 / 2) :
    (∑ z ∈ S, Real.exp (-a * |(z : ℝ)|)) ≤ Real.exp (4 * Real.exp (-a)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.code_exp_sum_le line 166

Source documentation

Finite families of quantization codes inherit a product partition bound.

theorem code_exp_sum_le {β : Type v} [Fintype β] [DecidableEq β]
    (C : Finset (β → ℤ)) (a : ℝ) (ha : Real.exp (-a) ≤ 1 / 2) :
    (∑ c ∈ C, Real.exp (-a * ∑ i, |(c i : ℝ)|)) ≤
      Real.exp (4 * Fintype.card β * Real.exp (-a)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.code_card_le line 192

Source documentation

A cost bound controls the number of possible quantization codes.

theorem code_card_le {β : Type v} [Fintype β] [DecidableEq β]
    (C : Finset (β → ℤ)) {a M : ℝ} (ha0 : 0 ≤ a)
    (ha : Real.exp (-a) ≤ 1 / 2) (hM : ∀ c ∈ C, (∑ i, |(c i : ℝ)|) ≤ M) :
    (C.card : ℝ) ≤ Real.exp (a * M + 4 * Fintype.card β * Real.exp (-a)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.hamming_exp_sum line 212

Source documentation

Partition function of Hamming distance on the Boolean cube.

theorem hamming_exp_sum {α : Type u} [Fintype α] [DecidableEq α]
    (x : α → Bool) (a : ℝ) :
    (∑ y : α → Bool, Real.exp (-a * hammingDist x y)) =
      (1 + Real.exp (-a)) ^ Fintype.card α := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.hamming_small_family_card line 229

Source documentation

A small Hamming ball occupies exponentially less than the whole cube.

theorem hamming_small_family_card {α : Type u} [Fintype α] [DecidableEq α]
    (G : Finset (α → Bool)) (x : α → Bool)
    (hG : ∀ y ∈ G, (hammingDist x y : ℝ) ≤ (Fintype.card α : ℝ) / 16) :
    (G.card : ℝ) ≤ Real.exp (3 * Fintype.card α / 8) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.card_good_cost line 271

Source documentation

A nonnegative cost with small average is small on at least half a finite set.

theorem card_good_cost {γ : Type w} [Fintype γ] [DecidableEq γ]
    (f : γ → ℝ) (hf : ∀ x, 0 ≤ f x) {M : ℝ} (hM : 0 < M)
    (hsum : (∑ x, f x) ≤ (Fintype.card γ : ℝ) * M / 2) :
    (Fintype.card γ : ℝ) / 2 ≤ ((Finset.univ.filter fun x ↦ f x ≤ M).card : ℝ) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.exists_same_code_far line 294

Source documentation

A large set of Boolean vectors contains a far pair with the same low-cost code.

theorem exists_same_code_far {α : Type u} {β : Type v} [Fintype α] [DecidableEq α]
    [Fintype β] [DecidableEq β] (G : Finset (α → Bool))
    (code : (α → Bool) → β → ℤ) {a M : ℝ} (ha0 : 0 ≤ a)
    (ha : Real.exp (-a) ≤ 1 / 2)
    (hcost : ∀ x ∈ G, (∑ i, |(code x i : ℝ)|) ≤ M)
    (hlarge : Real.exp (a * M + 4 * Fintype.card β * Real.exp (-a) +
      3 * Fintype.card α / 8) < (G.card : ℝ)) :
    ∃ x ∈ G, ∃ y ∈ G, code x = code y ∧
      (Fintype.card α : ℝ) / 16 < (hammingDist x y : ℝ) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.entropy_log_parameters line 337
Source documentation
Numerical entropy estimates, with fixed generous absolute constants.
```
theorem entropy_log_parameters {s R : ℝ} (hs : 0 < s) (hsR : s ≤ R) :
    let L := Real.log (16 * R / s)
…
```
theorem OAI.AsymptoticallyMinimalLittlewood.exp_small_lt_half_cube line 400
Source documentation
The Boolean cube is larger than the entropy bounds used above.
```
theorem exp_small_lt_half_cube {n : ℕ} (hn : 32 ≤ n) :
    Real.exp (13 * n / 32) < (2 : ℝ) ^ n / 2 := by
…
```

theorem OAI.AsymptoticallyMinimalLittlewood.exists_signings_same_round line 419

Source documentation

Entropy supplies two widely separated signings with identical rounded row sums.

theorem exists_signings_same_round {α : Type u} {β : Type v} [Fintype α] [DecidableEq α]
    [Fintype β] [DecidableEq β] (B : β → α → ℝ)
    (hB : ∀ i k, |B i k| ≤ 1) (hs : 32 ≤ Fintype.card α)
    (hsR : Fintype.card α ≤ Fintype.card β) :
    let d := 64 * Real.sqrt ((Fintype.card α : ℝ) *
…

theorem OAI.AsymptoticallyMinimalLittlewood.exists_partial_coloring line 506

Source documentation

A zero-start partial coloring fixes a fixed positive fraction of all coordinates.

theorem exists_partial_coloring {α : Type u} {β : Type v} [Fintype α] [DecidableEq α]
    [Fintype β] [DecidableEq β] (B : β → α → ℝ)
    (hB : ∀ i k, |B i k| ≤ 1) (hs : 0 < Fintype.card α)
    (hsR : Fintype.card α ≤ Fintype.card β) :
    ∃ z : α → ℝ, (∀ k, z k = -1 ∨ z k = 0 ∨ z k = 1) ∧
      (Fintype.card α : ℝ) / 16 ≤ ((Finset.univ.filter fun k ↦ z k ≠ 0).card : ℝ) ∧
      ∀ i, |∑ k, B i k * z k| ≤ 64 * Real.sqrt ((Fintype.card α : ℝ) *
        Real.log (16 * Fintype.card β / Fintype.card α)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.discrepancy_potential_contract line 587

Source documentation

The logarithmic discrepancy potential contracts on shortening the remaining columns.

theorem discrepancy_potential_contract {s u R : ℝ} (hs : 0 < s) (hsR : s ≤ R)
    (hu0 : 0 ≤ u) (hu : u ≤ (15 / 16) * s) :
    Real.sqrt (u * Real.log (16 * R / u)) ≤
      (63 / 64) * Real.sqrt (s * Real.log (16 * R / s)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.matrix_signing_raw line 631

Source documentation

Iterating the zero-start partial coloring proves the square-root logarithmic matrix bound.

theorem matrix_signing_raw (n : ℕ) :
    ∀ {α : Type u} {β : Type v} [Fintype α] [DecidableEq α]
      [Fintype β] [DecidableEq β], Fintype.card α = n →
      ∀ B : β → α → ℝ, (∀ i k, |B i k| ≤ 1) → Fintype.card α ≤ Fintype.card β →
      ∃ ξ : α → ℝ, (∀ k, ξ k = -1 ∨ ξ k = 1) ∧
        ∀ i, |∑ k, B i k * ξ k| ≤ 4096 * Real.sqrt ((Fintype.card α : ℝ) *
          Real.log (16 * Fintype.card β / Fintype.card α)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.matrix_signing line 713

theorem OAI.AsymptoticallyMinimalLittlewood.matrix_signing_nonpos line 745

Source documentation

Reversing a signing preserves discrepancy and allows its total sum to be nonpositive.

theorem matrix_signing_nonpos {α : Type u} {β : Type v}
    [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (B : β → α → ℝ) (hB : ∀ i k, |B i k| ≤ 1)
    (hsR : Fintype.card α ≤ Fintype.card β) :
    ∃ ξ : α → ℝ, (∀ k, ξ k = -1 ∨ ξ k = 1) ∧ (∑ k, ξ k) ≤ 0 ∧
      ∀ i, |∑ k, B i k * ξ k| ≤ 8192 * Real.sqrt ((Fintype.card α : ℝ) *
        Real.log (2 * Fintype.card β / Fintype.card α)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.dyadic_potential_bound line 764

Source documentation

The small mass controls the discrepancy potential at every dyadic scale.

theorem dyadic_potential_bound {s μ R : ℝ} (hμ : 0 < μ) (hμR : 2 * μ ≤ R)
    (hs : 0 ≤ s) (j : ℕ) (hsmass : s ≤ 2 ^ j * μ) :
    Real.sqrt (s * Real.log (2 * R / s)) / 2 ^ j ≤
      (3 / 4) ^ j * Real.sqrt (μ * Real.log (2 * R / μ)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.dyadic_round_step line 811

Source documentation

One mass-nonincreasing dyadic rounding step, on the exact odd coordinates.

theorem dyadic_round_step {α : Type u} {β : Type v}
    [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (A : β → α → ℝ) (hA : ∀ i k, |A i k| ≤ 1)
    (hαβ : Fintype.card α ≤ Fintype.card β)
    (a : α → ℕ) (j : ℕ) (ha : ∀ k, a k ≤ 2 ^ (j + 1))
    {μ : ℝ} (hμ : 0 < μ) (hμR : 2 * μ ≤ Fintype.card β)
    (hmass : (∑ k, (a k : ℝ) / 2 ^ (j + 1)) ≤ μ) :
    ∃ b : α → ℕ, (∀ k, b k ≤ 2 ^ j) ∧
      (∑ k, (b k : ℝ) / 2 ^ j) ≤ (∑ k, (a k : ℝ) / 2 ^ (j + 1)) ∧
      ∀ i, |∑ k, A i k * ((b k : ℝ) / 2 ^ j - (a k : ℝ) / 2 ^ (j + 1))| ≤
        8192 * ((3 / 4) ^ (j + 1) * Real.sqrt
          (μ * Real.log (2 * Fintype.card β / μ))) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.dyadic_round line 920

Source documentation

Iteration of the dyadic steps. The mass bound is maintained, not reset at each scale.

theorem dyadic_round {α : Type u} {β : Type v}
    [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (A : β → α → ℝ) (hA : ∀ i k, |A i k| ≤ 1)
    (hαβ : Fintype.card α ≤ Fintype.card β)
    {μ : ℝ} (hμ : 0 < μ) (hμR : 2 * μ ≤ Fintype.card β) (j : ℕ) :
    ∀ a : α → ℕ, (∀ k, a k ≤ 2 ^ j) →
      (∑ k, (a k : ℝ) / 2 ^ j) ≤ μ →
      ∃ b : α → ℕ, (∀ k, b k ≤ 1) ∧
        (∑ k, (b k : ℝ)) ≤ (∑ k, (a k : ℝ) / 2 ^ j) ∧
        ∀ i, |∑ k, A i k * ((b k : ℝ) - (a k : ℝ) / 2 ^ j)| ≤
          8192 * (3 * (1 - (3 / 4) ^ j) * Real.sqrt
            (μ * Real.log (2 * Fintype.card β / μ))) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.matrix_defect_rounding line 961

Source documentation

Defect-sensitive rounding on a real matrix, prior to the circle discretization.

theorem matrix_defect_rounding {α : Type u} {β : Type v}
    [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (A : β → α → ℝ) (hA : ∀ i k, |A i k| ≤ 1)
    (hαβ : Fintype.card α ≤ Fintype.card β)
    (p : α → ℝ) (hp : ∀ k, 0 ≤ p k ∧ p k ≤ 1)
    {μ : ℝ} (hμ : 0 < μ) (hμR : 2 * μ ≤ Fintype.card β)
    (hmass : (∑ k, p k) ≤ μ) :
    ∃ p' : α → ℝ, (∀ k, p' k = 0 ∨ p' k = 1) ∧ (∑ k, p' k) ≤ ∑ k, p k ∧
      ∀ i, |∑ k, A i k * (p' k - p k)| ≤
        1 + 24576 * Real.sqrt (μ * Real.log (2 * Fintype.card β / μ)) := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.grid_power_orthogonality line 1039

Source documentation

Orthogonality of the exact full root-of-unity grid.

theorem grid_power_orthogonality {M a b : ℕ} [NeZero M] (ha : a < M) (hb : b < M) :
    (∑ j : ZMod M, ZMod.stdAddChar j ^ a * conj (ZMod.stdAddChar j ^ b)) =
      if a = b then (M : ℂ) else 0 := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.grid_dirichlet_square line 1059

Source documentation

Mean square of a translated Dirichlet kernel on an oversampling grid.

theorem grid_dirichlet_square {M n : ℕ} [NeZero M] (hn : n ≤ M)
    {z : ℂ} (hz : ‖z‖ = 1) :
    (∑ j : ZMod M, ‖∑ a : Fin n, z ^ (a : ℕ) * conj (ZMod.stdAddChar j ^ (a : ℕ))‖ ^ 2) =
      (M : ℝ) * n := by
…

def OAI.AsymptoticallyMinimalLittlewood.gridDirichlet line 1105
Source documentation
A rotated, finite Dirichlet kernel on the root grid.
```
def gridDirichlet {M : ℕ} [NeZero M] (n : ℕ) (z : ℂ) (j : ZMod M) : ℂ :=
…
```

theorem OAI.AsymptoticallyMinimalLittlewood.grid_reproduce_monomial line 1109

Source documentation

The cross-Dirichlet kernel reproduces each required nonnegative frequency.

theorem grid_reproduce_monomial {M N : ℕ} [NeZero M] (hNM : 2 * N ≤ M)
    (k : Fin N) {z : ℂ} (hz : ‖z‖ = 1) :
    (∑ j : ZMod M, ZMod.stdAddChar j ^ (k : ℕ) * gridDirichlet (2 * N) z j *
      conj (gridDirichlet N z j)) = (M : ℂ) * N * z ^ (k : ℕ) := by
…

Mentions: OAI.AsymptoticallyMinimalLittlewood.gridDirichlet

theorem OAI.AsymptoticallyMinimalLittlewood.polynomial_grid_bound line 1166

Source documentation

No logarithmic loss: an oversampled analytic polynomial is controlled on the whole circle.

theorem polynomial_grid_bound {N M : ℕ} [NeZero M] (hN : 0 < N) (hNM : 2 * N ≤ M)
    (c : Fin N → ℂ) {G : ℝ} (hG : 0 ≤ G)
    (hgrid : ∀ j : ZMod M, ‖∑ k : Fin N, c k * ZMod.stdAddChar j ^ (k : ℕ)‖ ≤ G)
    {z : ℂ} (hz : ‖z‖ = 1) :
    ‖∑ k : Fin N, c k * z ^ (k : ℕ)‖ ≤ 2 * G := by
…

def OAI.AsymptoticallyMinimalLittlewood.defectMass line 1222
theorem OAI.AsymptoticallyMinimalLittlewood.defect_rounding line 1225