OAI/Analysis/FourierLLogL/Paths/Troupe.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Grade line 19
2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stage line 22
3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.grade line 23
4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.amount line 26

   Source documentation

   height parameter allowing very small mass static entries.

   def amount (s : Scene M) (j : ℕ) := height j+max (-log s.norm) 0+2

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.rose line 27
6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.recital line 28
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.rec_one line 30
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.amount_limits line 32
9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.entitled line 37
10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.cutBook line 39
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.cut_nonneg line 41
12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.cover_limit line 49
13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.boom line 64
14. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.burst line 65
15. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.showScore line 67
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.burst_pos line 72
17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.show_one line 75
18. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.sticker line 84
19. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.paint_birth line 88

    Source documentation

    summing conditional estimate-envelope costs over births.

    lemma paint_birth :
        ∀ᶠ j : ℕ in atTop, ∀ (M J : ℕ) (s : Scene M)
          (t : Thread M s) (f : Grid M → ℝ) (p : Plot),
          Following j J f t → Fit s → entitled (grade p) s j →
          (∀ x, f x ≤ exp (height j)) → ∀ c : Board M,
            stats t (showScore p c j) ≤ 1+sticker s (grade p) j*stats t (minted p c) := by
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Thread, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.Fit, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.entitled, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.grade, OAI.FourierLLogL.Dyadic.Procedure.Paths.stats, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.showScore, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.sticker