noncomputable def Frourio.S (Λ : ℝ) (n : ℤ) : ℝ

構造列 S_n = Λ^n - Λ^{-n}

Equations

• Frourio.S Λ n = Λ ^ n - Λ ^ (-n)

theorem Frourio.S_neg (Λ : ℝ) (n : ℤ) : S Λ (-n) = -S Λ n

S_n の基本的な性質：S_{-n} = -S_n

@[simp]

theorem Frourio.S_zero (Λ : ℝ) : S Λ 0 = 0

S_0 = 0

theorem Frourio.S_one (Λ : ℝ) : S Λ 1 = Λ - 1 / Λ

S_1 の値

theorem Frourio.S_add (Λ : ℝ) (hΛ : 0 < Λ) (m n : ℤ) : S Λ (m + n) = S Λ m * Λ ^ n + S Λ n * Λ ^ (-m)

S_n の加法公式: S_{m+n} = S_m Λ^n + S_n Λ^{-m}

theorem Frourio.two_sinh_neg (t : ℝ) : 2 * Real.sinh (-t) = -(2 * Real.sinh t)

Helper: 2 * sinh is odd.

D1: Hyperbolic representation via exponential identities.

theorem Frourio.exp_nat_mul_log_eq_pow (Λ : ℝ) (hΛpos : 0 < Λ) (n : ℕ) : Real.exp (↑n * Real.log Λ) = Λ ^ n

Helper: exp of a natural multiple of log equals pow.

theorem Frourio.S_as_exp_sub_exp_neg_ofNat (Λ : ℝ) (hΛpos : 0 < Λ) (n : ℕ) : S Λ ↑n = Real.exp (↑n * Real.log Λ) - Real.exp (-(↑n * Real.log Λ))

Exponential-difference form for natural indices.

theorem Frourio.S_as_sinh_ofNat (Λ : ℝ) (hΛpos : 0 < Λ) (n : ℕ) : S Λ ↑n = 2 * Real.sinh (↑n * Real.log Λ)

Hyperbolic form via sinh for natural indices.

theorem Frourio.S_as_sinh_int (Λ : ℝ) (hΛpos : 0 < Λ) (m : ℤ) : S Λ m = 2 * Real.sinh (↑m * Real.log Λ)

Hyperbolic form via sinh for integer indices.

Basic inequalities derived from the exponential form (Λ > 1).

theorem Frourio.S_nonneg_of_nat (Λ : ℝ) (hΛgt1 : 1 < Λ) (n : ℕ) : 0 ≤ S Λ ↑n

theorem Frourio.S_pos_of_nat_pos (Λ : ℝ) (hΛgt1 : 1 < Λ) {n : ℕ} (hn : 0 < n) : 0 < S Λ ↑n

theorem Frourio.S_ne_zero_of_pos_ne_one (Λ : ℝ) (hΛpos : 0 < Λ) (hΛne1 : Λ ≠ 1) {n : ℕ} (hn : 0 < n) : S Λ ↑n ≠ 0