Freeze.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FourierLLogL.Compress.average_two_below line 14

lemma OAI.FourierLLogL.Compress.large_heat line 24

Source documentation

A small noisy cost implies a large heat sum (Gibbs comparison).

lemma large_heat (P : Law Ω) (q : Law A) (X : Ω → A) (tag : A → G) (U : Ω → G) (c : G → ℝ)
    (hcov : (P.send X).dominated q) (F : ℝ)
    (hF : P.Ex (fun x => -log (q (X x))) - P.Hcond X (fun x => tag (X x)+U x)+
      P.Ex (fun x => c (U x)) ≤ F) :
    ∃ z : G, exp (-F) ≤ q.Ex fun a => exp (-c (z-tag a)) := by
…

Mentions: OAI.FourierLLogL.Law

lemma OAI.FourierLLogL.Compress.stack_select line 75

Source documentation

Stack selection with one coordinate per actual letter.

lemma stack_select (tag : A → G) (c : G → ℝ) (hc : ∀ x, 0 ≤ c x)
    (p : Law (A×V)) (P : Law Ω) (X : Ω → I → A) (W : Ω → I → V) (U : Ω → G)
    (hp : ∀ i : I, P.send (fun x => (X x i,W x i)) = p)
    (F D : ℝ) (hF : 0 < F) (hD : 0 < D)
    [Nonempty I]
    (hs : Fintype.card I * p.Hcond Prod.fst Prod.snd -
      P.Hcond X (fun x => (ans tag X U x, W x)) + P.Ex (fun x => c (U x)) ≤ F)
    (hd : log (Fintype.card A) - p.Hcond Prod.fst Prod.snd ≤ D) :
    ∃ (q : I → Law A) (z : G),
      exp (-(2*F)) ≤ (pack q).Ex (fun x => exp (-c (z-tot tag x))) ∧
      ∑ i, (log (Fintype.card A)- (q i).entropy) ≤ 2*(Fintype.card I*D) := by
…

Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.ans, OAI.FourierLLogL.Compress.tot

lemma OAI.FourierLLogL.Compress.freeze line 154