OAI/Analysis/FourierLLogL/Assembly/Receipt.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.parody line 19
2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stampAux line 20
3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stamp line 24
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stamp_nonneg line 26
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.chamber_fee line 35
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.receipt_main line 43
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.receipt_static line 65
8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.gateTax line 69
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tax_pos line 72
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.receipt_paid line 76
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.parody_fee line 142

    Source documentation

    pointwise price comparison for expected flags.

    lemma parody_fee (s : Scene M) (j : ℕ) (i : ℕ) (h : i ≤ mainIx j+1) :
        parody s i ≤ 10^6*Thermal.H j^32*surcharge s true (i-1) := by
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.parody, OAI.FourierLLogL.Dyadic.Thermal.H, OAI.FourierLLogL.Dyadic.Procedure.surcharge

12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.depth_rate_fee line 169