OAI/Analysis/FourierLLogL/Assembly/Chill.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.drought line 19
2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.drought_pos line 20
3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.chargeStatic line 21
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.charge_pos line 23
5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.coldLump line 30
6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.coldFee line 31
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.chill_descendants line 34
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.frostCompare line 121

   Source documentation

   Every coast including virtual ends of the true live processing bills only once for static descendants.

   lemma frostCompare :
       ∀ᶠ j : ℕ in atTop, ∀ M J : ℕ, ∀ f : Grid M → ℝ, ∀ s : Scene M,
       ∀ t : Play j M s, Play.Follows J f t → s.live=true →
   
         netGross t ≤ (trace false t).flatFee billOf + coldFee (trace false t) := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Play, OAI.FourierLLogL.Dyadic.Procedure.Play.Follows, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.netGross, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.billOf, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.coldFee