Rent.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Cost of a coupling of contextual rows

def OAI.FourierLLogL.Compress.ctxt line 17
Source documentation
Context part of a vector of full rows.
```
def ctxt (w : A → V) (X : Ω → I → A) (a : Ω) (i : I) := w (X a i)
```
def OAI.FourierLLogL.Compress.readP line 18
def OAI.FourierLLogL.Compress.rent line 21
Source documentation
Contextual cost of a coupling with tag-sum output and random error ø of alphabet E.
```
def rent (tag : A → G) (w : A → V) (u : E → G) (c : E → ℝ)
    (P : Law Ω) (X : Ω → I → A) (U : Ω → E) :=
…
```
Mentions: OAI.FourierLLogL.Law
def OAI.FourierLLogL.Compress.hasRows line 27
lemma OAI.FourierLLogL.Compress.rent_first line 31
lemma OAI.FourierLLogL.Compress.rent_nonneg line 40
lemma OAI.FourierLLogL.Compress.rent_send line 50
lemma OAI.FourierLLogL.Compress.rent_cont line 57
def OAI.FourierLLogL.Compress.opt line 64
Source documentation
Min rent uses r rows.
```
def opt (n : ℕ) (p : Law A) (tag : A → G) (w : A → V) (u : E → G) (c : E → ℝ) :=
…
```
Mentions: OAI.FourierLLogL.Law
lemma OAI.FourierLLogL.Compress.opt_spec line 68
lemma OAI.FourierLLogL.Compress.opt_le_rent line 89
lemma OAI.FourierLLogL.Compress.opt_nonneg line 100
lemma OAI.FourierLLogL.Compress.Hcond_function line 107

lemma OAI.FourierLLogL.Compress.Hcond_reduce line 115

Source documentation

Chain rule for deterministic reduction f(X).

lemma Hcond_reduce (P : Law Ω) (X : Ω → A) (W : Ω → V) (f : A → B) :
    P.Hcond X W = P.Hcond X (fun x => (f (X x),W x)) + P.Hcond (fun x => f (X x)) W := by
…

Mentions: OAI.FourierLLogL.Law

lemma OAI.FourierLLogL.Compress.rent_antitone line 126

Source documentation

Improving contexts, for the same full rows and tag, reduces the rent.

lemma rent_antitone (tag : A → G) (w : A → V) (w' : A → W) (u : E → G) (c : E → ℝ)
    (p : V → W) (h : w' = p ∘ w)
    (P : Law Ω) (X : Ω → I → A) (U : Ω → E) :
    rent tag w u c P X U ≤ rent tag w' u c P X U := by
…

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