OAI/Analysis/FourierLLogL/Paths/Ray.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.content line 17
2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray line 18
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.content_pos line 20
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray_pos line 21
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray_sq line 22
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray_bounds line 24
7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.glow line 33

   Source documentation

   Unit linearization of an output triple

   def glow (v w : ℂ) (x : ℝ) (a b : ℂ) (t : ℝ) :=
   …

8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.glow_add line 36
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.glow_scale line 39
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.glow_limit line 43
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray_shift line 64
12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.ray_slide line 88
13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.prism line 106
14. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.watt line 108
15. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yieldW line 109
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yield_step line 110
17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.watt_idle line 113
18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.watt_slide line 125