OAI/Analysis/FourierLLogL/Finite/Alternative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Law.continuous_pdf line 13
2. lemma OAI.FourierLLogL.Law.continuous_entropy line 16
3. lemma OAI.FourierLLogL.Law.continuous_Ex line 20
4. lemma OAI.FourierLLogL.Law.continuous_prob line 23
5. lemma OAI.FourierLLogL.Law.continuous_send_pdf line 26
6. lemma OAI.FourierLLogL.Law.continuous_send line 29
7. lemma OAI.FourierLLogL.Law.continuous_H line 33
8. lemma OAI.FourierLLogL.Law.continuous_Hcond line 36
9. lemma OAI.FourierLLogL.Law.primal_feasible line 42

   Source documentation

   Convex minimization over finite distributions with a linear constraint g=0: if any dual objective (arbitrary multipliers) is at most C somewhere, there is a constrained law with value at most C.

   lemma primal_feasible {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       (f : Law α → ℝ) (hf : Continuous f)
       (g : Law α → E) (hg : Continuous g)
       (hfc : ∀ P Q t h0 h1, f (mixture P Q t h0 h1) ≤ t*f P+(1-t)*f Q)
       (hgc : ∀ P Q t h0 h1, g (mixture P Q t h0 h1) = t • g P+(1-t) • g Q)
       (hP : ∃ P, g P = 0)
       (C : ℝ) (hC : ∀ L : E →L[ℝ] ℝ, ∃ P, f P + L (g P) ≤ C) :
       ∃ P, f P ≤ C ∧ g P = 0 := by
   …

   Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.mixture