AffineEntropyNat.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Entropy bound for a possibly empty finite signature set

The natural count may vanish. Taking its maximum with one lets the same uniform entropy bound feed the sparse-perturbation budget in that case.

theorem OAI.QuantitativeVanDerWaerden.Parameters.affine_nat_entropy_bound line 18

Source documentation

Natural signature counts obey the maximum-with-one entropy bound, including the empty signature set. The finite counting premise is used unchanged.

theorem affine_nat_entropy_bound {k T : ℕ} (hk : 32 ≤ k)
    {G q A : ℝ} (hG : 1 ≤ G) (hq : 1 ≤ q) (hA : 0 ≤ A)
    (hcount : (T : ℝ) ≤ 25 * G *
      ((k : ℝ) * ((dimension k : ℝ) * q ^ 2 + 1) + 1) ^ 8)
    (hglobal : Real.log G ≤
      A * (k : ℝ) ^ (3 / 10 : ℝ) * Real.log (k : ℝ))
    (hprime : Real.log q ≤
      4 * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log (k : ℝ)) :
    Real.log (max 1 (T : ℝ)) ≤
      (A + 108) * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log (k : ℝ) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension