IsNormalized

formal source

 594  ∀ x : ℝ, 0 < x → F x = F x⁻¹
 595
 596/-- **Normalized**: F(1) = 0. -/
 597def IsNormalized (F : ℝ → ℝ) : Prop := F 1 = 0
 598
 599/-- **Calibration (Condition 1.2)**:
 600lim_{t→0} 2·F(e^t)/t² = 1, equivalently G''(0) = 1 where G(t) = F(e^t). -/
 601def IsCalibrated (F : ℝ → ℝ) : Prop :=
 602  deriv (deriv (G F)) 0 = 1
 603
 604/-- **Calibration (limit form)**:
 605lim_{t→0} 2·F(e^t)/t² = 1, expressed on H = G + 1. -/
 606def IsCalibratedLimit (F : ℝ → ℝ) : Prop :=
 607  HasLogCurvature (H F) 1
 608
 609lemma taylorWithinEval_succ_real (H : ℝ → ℝ) (n : ℕ) (x₀ x : ℝ) :
 610  taylorWithinEval H (n + 1) Set.univ x₀ x =
 611    taylorWithinEval H n Set.univ x₀ x +
 612      (((n + 1 : ℝ) * (Nat.factorial n))⁻¹ * (x - x₀) ^ (n + 1)) *
 613        iteratedDerivWithin (n + 1) H Set.univ x₀ := by
 614  simpa [smul_eq_mul] using taylorWithinEval_succ H n Set.univ x₀ x
 615
 616lemma taylorWithinEval_one_univ (H : ℝ → ℝ) (x : ℝ) :
 617  taylorWithinEval H 1 Set.univ 0 x = H 0 + deriv H 0 * x := by
 618  have h := taylorWithinEval_succ_real H 0 0 x
 619  -- simplify the Taylor term at order 1
 620  have h' :
 621      taylorWithinEval H 1 Set.univ 0 x = H 0 + x * deriv H 0 := by
 622    simp [taylor_within_zero_eval, iteratedDerivWithin_univ, iteratedDerivWithin_one,
 623      iteratedDeriv_one, derivWithin_univ, sub_eq_add_neg] at h
 624    simpa [mul_comm] using h
 625  simpa [mul_comm] using h'
 626
 627lemma taylorWithinEval_two_univ (H : ℝ → ℝ) (x : ℝ) :