AveragingBounds

formal source

  54  have hx : 0 < Real.exp t := Real.exp_pos t
  55  simpa [Real.exp_neg] using (SymmUnit.symmetric (F:=F) hx)
  56
  57class AveragingBounds (F : ℝ → ℝ) : Prop extends SymmUnit F where
  58  upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
  59  lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
  60
  61theorem agrees_on_exp_of_bounds {F : ℝ → ℝ} [AveragingBounds F] :
  62    AgreesOnExp F := by
  63  intro t
  64  have h₁ := AveragingBounds.upper (F:=F) t
  65  have h₂ := AveragingBounds.lower (F:=F) t
  66  have : F (Real.exp t) = Jcost (Real.exp t) := le_antisymm h₁ h₂
  67  simpa using this
  68
  69theorem F_eq_J_on_pos_alt (F : ℝ → ℝ)
  70  (hAgree : AgreesOnExp F) : ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  71  intro x hx
  72  have : ∃ t, Real.exp t = x := ⟨Real.log x, by simpa using Real.exp_log hx⟩
  73  rcases this with ⟨t, rfl⟩
  74  simpa using hAgree t
  75
  76instance (priority := 90) averagingDerivation_of_bounds {F : ℝ → ℝ} [AveragingBounds F] :
  77    AveragingDerivation F :=
  78  { toSymmUnit := (inferInstance : SymmUnit F)
  79  , agrees := agrees_on_exp_of_bounds (F:=F) }
  80
  81def mkAveragingBounds (F : ℝ → ℝ)
  82  (symm : SymmUnit F)
  83  (upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t))
  84  (lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)) :
  85  AveragingBounds F :=
  86{ toSymmUnit := symm, upper := upper, lower := lower }
  87