131structure LogAczelData (G : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop where 132 continuous_G : Continuous G 133 zero_G : G 0 = 0 134 even_G : Function.Even G 135 continuous_P : Continuous (Function.uncurry P) 136 symmetric_P : ∀ u v, P u v = P v u 137 aczel_eq : ∀ t u : ℝ, G (t + u) + G (t - u) = P (G t) (G u) 138 139/-- Continuity of the derived cost on positive ratios lifts to continuity of 140the log-coordinate cost `G(t) = F(exp t)`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.