OAI/Analysis/FourierLLogL/Thermal/True.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

True-law estimates used to supervise all attempts

  1. def OAI.FourierLLogL.Dyadic.Thermal.Update.quiet line 17

    Source documentation

    Failure of loudness only.

    def quiet (u : Update j M p) (x : Clutch j M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Update, OAI.FourierLLogL.Dyadic.Thermal.Clutch

  2. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.consistent_triangle line 20
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.diff_cost line 33
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.quiet_scale line 62