OAI/Analysis/FourierLLogL/Capture/Dual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Capture.utility line 15
2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.sales line 18
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.utility_bounds line 21
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.utility_diff line 29
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.income line 41
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.fz_dry line 69
7. def OAI.FourierLLogL.Dyadic.Procedure.Capture.seller line 74
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.seller_limit line 76
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.price_upper line 84
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.seller_eq line 95
11. theorem OAI.FourierLLogL.Dyadic.Procedure.Capture.test_complete line 107

    Source documentation

    sales of every packet at most the magnitude, attained by choice of a bounded tester.

    theorem test_complete (main : Bool) (s : Scene M) (hp : 0 ≤ s.wage) (hv : 0 ≤ s.norm)
        (i : Grid M) :
        (∀ c : Grid M → ℂ, (∀ z, ‖c z‖ ≤ 1) → sales main s c i ≤ magnitude main s i) ∧
          ∃ c : Grid M → ℂ, (∀ z, ‖c z‖ ≤ 1) ∧ sales main s c i = magnitude main s i := by
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Capture.sales, OAI.FourierLLogL.Dyadic.Procedure.Capture.magnitude

12. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.sup_children line 144