SymmUnit

formal source

  39    symm; simp [Real.exp_neg t]
  40  simp [Jcost, h]
  41
  42class SymmUnit (F : ℝ → ℝ) : Prop where
  43  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
  44  unit0 : F 1 = 0
  45
  46class AveragingAgree (F : ℝ → ℝ) : Prop where
  47  agrees : AgreesOnExp F
  48
  49class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
  50  agrees : AgreesOnExp F
  51
  52lemma even_on_log_of_symm {F : ℝ → ℝ} [SymmUnit F] (t : ℝ) :
  53    F (Real.exp t) = F (Real.exp (-t)) := by
  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⟩