OAI/Analysis/FourierLLogL/Snapshot/Difference.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.grain line 15
2. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.cloud line 16
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.grain_nonneg line 18
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.cloud_nonneg line 21
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.cloud_same line 24
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.distance_cloud line 26
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.shift_formula line 38
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.grain_shrinks line 41
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.grain_average line 60

   Source documentation

   comparison curvature cost at a spatial step is controlled by the Fisher charge

   lemma grain_average (a b m t : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : 0 ≤ t)
       (h : a+b=2*m) :
       (grain a t+grain b t)/2 ≤ grain m t +4*((a-b)/2)^2/m := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Snapshot.grain

10. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.cloud_kill line 93
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.cloud_drift line 102