same_fixed_point

formal source

  70  unfold h; positivity
  71
  72/-- g and h share the same fixed point at t = 0. -/
  73theorem same_fixed_point : g 0 = 0 ∧ h 0 = 0 := ⟨g_at_zero, h_at_zero⟩
  74
  75/-- Both g and h are even functions. -/
  76theorem same_symmetry : ∀ t, g t = g (-t) ∧ h t = h (-t) :=
  77  fun t => ⟨g_even t, h_even t⟩
  78
  79structure JCostLogSpaceCert where
  80  g_zero : g 0 = 0
  81  g_even : ∀ t, g t = g (-t)
  82  g_positive : ∀ {t : ℝ}, t ≠ 0 → 0 < g t
  83  h_zero : h 0 = 0
  84  h_even : ∀ t, h t = h (-t)
  85  h_nonneg : ∀ t, 0 ≤ h t
  86  same_fixed_pt : g 0 = 0 ∧ h 0 = 0
  87  same_sym : ∀ t, g t = g (-t) ∧ h t = h (-t)
  88
  89noncomputable def jCostLogSpaceCert : JCostLogSpaceCert where
  90  g_zero := g_at_zero
  91  g_even := g_even
  92  g_positive := g_pos_off_zero
  93  h_zero := h_at_zero
  94  h_even := h_even
  95  h_nonneg := h_nonneg
  96  same_fixed_pt := same_fixed_point
  97  same_sym := same_symmetry
  98
  99end IndisputableMonolith.Foundation.JCostConvexityInLogSpace