OAI/Analysis/FourierLLogL/Compress/Theorem.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Compress.init_gap line 16
2. lemma OAI.FourierLLogL.Compress.compress_arrays line 27

   Source documentation

   Finite compression from schedule and numerical constraints, before a choice of scales in terms of height.

   lemma compress_arrays (tag : A → G) (hi : Injective tag) (q : Law G)
       (hq : ∀ x, 0 < q x) (c : G → ℝ) (hc : ∀ x, 0 ≤ c x) (hc0 : c 0=0)
       (Q : Law Θ) (χ : Θ → AddChar G ℂ) (hn : ∀ t x, ‖χ t x‖=1)
       (hrq : ∀ g, (↑(exp (-c g)):ℂ)=Q.Cx fun t => χ t g)
       (hlog : ∀ g, -log (q g) = -log (q 0) + c g)
       (F L C : ℝ) (hF : 1 ≤ F) (hL : 0 ≤ L)
       (T N m : ℕ) (hm : 0 < m) (hN : m ≤ N) (hT : 3*N ≤ T) (S : Schedule)
       (l u r : ℕ → ℕ)
       (hl : ∀ i, i < S.size → l i ≤ u i ∧ u i ≤ m ∧ 0 < u i ∧ 0 < r i ∧
         2*r i*l i ≤ N ∧ L ≤ (r i:ℝ)*(u i:ℝ))
       (hp : ∀ i j, i < j → j < S.size → u j ≤ l i ∧ r i ≤ r j)
       (hg : ∀ P : Law A, exp (-F) ≤ heatMoment (Fin T) P tag c)
   …

   Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.S, OAI.FourierLLogL.Compress.Schedule, OAI.FourierLLogL.Compress.heatMoment