IndisputableMonolith.Cost.JensenSketch

   1import IndisputableMonolith.Cost
   2
   3/-!
   4# JensenSketch (compatibility wrapper)
   5
   6Historically this module duplicated the `JensenSketch`/T5 interface.
   7The canonical definitions now live in `IndisputableMonolith/Cost.lean`.
   8
   9Importing `IndisputableMonolith.Cost.JensenSketch` is therefore equivalent to importing
  10`IndisputableMonolith.Cost`, with one small convenience instance retained below.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Cost
  15
  16/-- Convenience: `JensenSketch` bounds immediately give `AveragingAgree`, i.e.\
  17pointwise exp-axis agreement with `Jcost`. -/
  18instance (priority := 95) averagingAgree_of_jensen {F : ℝ → ℝ} [JensenSketch F] :
  19  AveragingAgree F :=
  20  ⟨by
  21    intro t
  22    exact le_antisymm (JensenSketch.axis_upper (F:=F) t) (JensenSketch.axis_lower (F:=F) t)⟩
  23
  24end Cost
  25end IndisputableMonolith
  26