def definition def or abbrev

`H_AczelClassification`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  82def H_AczelClassification : Prop :=

proof body

Definition body.

  83  ∀ (H : ℝ → ℝ),
  84    H 0 = 1 →
  85    Continuous H →
  86    (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
  87    ContDiff ℝ ⊤ H
  88
  89/-! ## §3 Integration Bootstrap: Continuous → C^∞ -/
  90
  91noncomputable section
  92

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

dAlembert_contDiff_top in IndisputableMonolith.Cost.AczelTheorem decl_use
h_aczel_classification_proved in IndisputableMonolith.Cost.AczelTheorem decl_use

depends on (2)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use