OAI/Analysis/FourierLLogL/Compress/Endpoint.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Compress.log_ticket line 12
2. lemma OAI.FourierLLogL.Compress.approx_error line 37
3. lemma OAI.FourierLLogL.Compress.size_bound line 90
4. theorem OAI.FourierLLogL.Compress.entropy_compression line 125

   Source documentation

   Compression at the scales in terms of d=2^j.

   theorem entropy_compression (D : ℝ) (hD : 1 ≤ D) :
       ∀ᶠ j : ℕ in atTop, ∀ (A G Θ : Type)
         (_ : Fintype A) (_ : Fintype G) (_ : Fintype Θ) (_ : Nonempty A)
         (_ : DecidableEq G) (_ : AddCommGroup G)
         (tag : A → G), Injective tag → ∀ (q : Law G), (∀ x, 0 < q x) →
         ∀ (c : G → ℝ), (∀ x, 0 ≤ c x) → c 0=0 →
         ∀ (Q : Law Θ) (χ : Θ → AddChar G ℂ),
           (∀ t x, ‖χ t x‖=1) →
           (∀ g, (↑(exp (-c g)):ℂ)=Q.Cx (fun t => χ t g)) →
           (∀ g, -log (q g) = -log (q 0) + c g) →
           -log (q 0) ≤ D*height j →
           (∀ n : ℕ, n ≤ 2^(2*j) → lnS (Fin n) tag ≤ height j * j^2) →
   …

   Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.lnS