noncomputable def selfConcordantOmega : ↑(Set.Ioi (-1)) → ℝ

Definition 5.0.21 (1): the auxiliary function ω(t) = t - log (1 + t) on (-1, ∞).

noncomputable def selfConcordantOmegaStar : ↑(Set.Iio 1) → ℝ

Definition 5.0.21 (2): the auxiliary function ω_*(τ) = -τ - log (1 - τ) on (-∞, 1).

noncomputable def selfConcordantOmegaDeriv : ↑(Set.Ioi (-1)) → ℝ

The derivative branch ω'(t) = t / (1 + t) of ω, defined on its natural domain (-1, ∞).

noncomputable def selfConcordantOmegaPrimeStar : ↑(Set.Iio 1) → ℝ

The inverse branch ω'_*(τ) = τ / (1 - τ) associated with ω and ω_*, defined on its natural domain (-∞, 1).

def SelfConcordantAuxiliaryFunction.termω : Lean.ParserDescr

def SelfConcordantAuxiliaryFunction.«termω_*» : Lean.ParserDescr

def SelfConcordantAuxiliaryFunction.termω' : Lean.ParserDescr

def SelfConcordantAuxiliaryFunction.«termω'_*» : Lean.ParserDescr

theorem mf_mul_lt_one_of_lt_inv {Mf : NNReal} {r : ℝ} (hr : r < 1 / ↑Mf) : ↑Mf * r < 1

If r < 1 / M_f, then the scaled quantity M_f r lies in the natural domain of ω_*.

theorem neg_one_lt_mf_mul_of_nonneg {Mf : NNReal} {r : ℝ} (hr : 0 ≤ r) : -1 < ↑Mf * r

If r ≥ 0, then the scaled quantity M_f r lies in the natural domain of ω.

def selfConcordantOmegaArg (Mf : NNReal) (r : ℝ) (hr : -1 < ↑Mf * r) : ↑(Set.Ioi (-1))

The canonical ω argument attached to a scalar r whose scaled value lies in the natural domain of ω.

@[simp]

theorem coe_selfConcordantOmegaArg (Mf : NNReal) (r : ℝ) (hr : -1 < ↑Mf * r) : ↑(selfConcordantOmegaArg Mf r hr) = ↑Mf * r

Coercing selfConcordantOmegaArg Mf r hr back to ℝ recovers M_f r.

noncomputable def selfConcordantOmegaOneHalfArg : ↑(Set.Ioi (-1))

The textbook point 1 / 2 in the natural domain (-1, ∞) of ω.

@[simp]

theorem coe_selfConcordantOmegaOneHalfArg : ↑selfConcordantOmegaOneHalfArg = 1 / 2

Coercing selfConcordantOmegaOneHalfArg back to ℝ recovers 1 / 2.

noncomputable def selfConcordantOmegaAtOneHalf : ℝ

The Chapter 5 textbook constant ω(1 / 2).

def selfConcordantOmegaStarArg (Mf : NNReal) (r : ℝ) (hr : ↑Mf * r < 1) : ↑(Set.Iio 1)

The canonical ω_* argument attached to a scalar r satisfying (Mf : ℝ) * r < 1.

@[simp]

theorem coe_selfConcordantOmegaStarArg (Mf : NNReal) (r : ℝ) (hr : ↑Mf * r < 1) : ↑(selfConcordantOmegaStarArg Mf r hr) = ↑Mf * r

Coercing selfConcordantOmegaStarArg Mf r hr back to ℝ recovers M_f r.

@[simp]

theorem selfConcordantOmega_apply (t : ↑(Set.Ioi (-1))) : selfConcordantOmega t = ↑t - Real.log (1 + ↑t)

Evaluating ω at a point of (-1, ∞) recovers the explicit formula t - log (1 + t).

@[simp]

theorem selfConcordantOmegaStar_apply (τ : ↑(Set.Iio 1)) : selfConcordantOmegaStar τ = -↑τ - Real.log (1 - ↑τ)

Evaluating ω_* at a point of (-∞, 1) recovers the textbook formula -τ - log (1 - τ).

@[simp]

theorem selfConcordantOmegaDeriv_apply (t : ↑(Set.Ioi (-1))) : selfConcordantOmegaDeriv t = ↑t / (1 + ↑t)

Evaluating ω' at a point of (-1, ∞) recovers the explicit derivative formula t / (1 + t).

@[simp]

theorem selfConcordantOmegaPrimeStar_apply (τ : ↑(Set.Iio 1)) : selfConcordantOmegaPrimeStar τ = ↑τ / (1 - ↑τ)

Evaluating ω'_* at a point of (-∞, 1) recovers the explicit inverse-branch formula τ / (1 - τ).