OAI/Analysis/FourierLLogL/Assembly/Festival.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.masked_split line 18
2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subt_le line 27
3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.crumb line 35
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.start_ico line 38
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scalar_stage line 44
6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.bigCrumb line 117
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.main_stage line 121

   Source documentation

   Main handles a contour interval, consuming the small leading prefix only once.

   lemma main_stage :
       ∀ᶠ j : ℕ in atTop, ∀ (M J : ℕ) (s : Scene M) (f : Grid M → ℝ) (x u : Grid M)
         (L : Path M), s.live=true → Cast j J f s L → Trip x s L →
           ∀ (v : ℝ),
             (∀ l r : Path M, L=l++r → (∀ i, i ≤ mainIx j → stall u (tagM i) j L l) →
               ‖subtotal (proceeds x u) l‖ ≤ v) →
             ‖subtotal (proceeds x u) L‖ ≤ v+10^20*fullFax L+
               bigCrumb 0 (mainIx j+1) j L := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Cast, OAI.FourierLLogL.Dyadic.Procedure.Paths.Trip, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stall, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tagM, OAI.FourierLLogL.Dyadic.Procedure.Paths.subtotal, OAI.FourierLLogL.Dyadic.Procedure.Paths.proceeds, OAI.FourierLLogL.Dyadic.Procedure.Paths.fullFax, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.bigCrumb

8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.souvenir line 177
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.gala line 182