Аналіз I, Розділ 9.2: Алгебра дійснозначних функцій

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Нагадування базових поелементних операцій над функціями.

@[reducible, inline]

noncomputable abbrev Chapter9.function_example : ℝ → ℝ

Equations

• Chapter9.function_example x = if x ∈ (fun (y : ℚ) => ↑y) '' Set.univ then 1 else 0

theorem Chapter9.add_func_eval (f g : ℝ → ℝ) (x : ℝ) : (f + g) x = f x + g x

Визначення 9.2.1 (Арифметичні операції над функціями)

theorem Chapter9.sub_func_eval (f g : ℝ → ℝ) (x : ℝ) : (f - g) x = f x - g x

theorem Chapter9.max_func_eval (f g : ℝ → ℝ) (x : ℝ) : max f g x = max (f x) (g x)

theorem Chapter9.min_func_eval (f g : ℝ → ℝ) (x : ℝ) : min f g x = min (f x) (g x)

theorem Chapter9.mul_func_eval (f g : ℝ → ℝ) (x : ℝ) : (f * g) x = f x * g x

theorem Chapter9.div_func_eval (f g : ℝ → ℝ) (x : ℝ) : (f / g) x = f x / g x

theorem Chapter9.smul_func_eval (c : ℝ) (f : ℝ → ℝ) (x : ℝ) : (c • f) x = c * f x

@[reducible, inline]

abbrev Chapter9.f_9_2_2 : ℝ → ℝ

Equations

• Chapter9.f_9_2_2 x = x ^ 2

@[reducible, inline]

abbrev Chapter9.g_9_2_2 : ℝ → ℝ

Equations

• Chapter9.g_9_2_2 x = 2 * x

def Chapter9.Exercise_9_2_1a : Decidable (∀ (f g h : ℝ → ℝ), (f + g) ∘ h = f ∘ h + g ∘ h)

Equations

• Chapter9.Exercise_9_2_1a = sorry

def Chapter9.Exercise_9_2_1b : Decidable (∀ (f g h : ℝ → ℝ), f ∘ (g + h) = f ∘ g + f ∘ h)

Equations

• Chapter9.Exercise_9_2_1b = sorry

def Chapter9.Exercise_9_2_1c : Decidable (∀ (f g h : ℝ → ℝ), (f + g) * h = f * h + g * h)

Equations

• Chapter9.Exercise_9_2_1c = sorry

def Chapter9.Exercise_9_2_1d : Decidable (∀ (f g h : ℝ → ℝ), f * (g + h) = f * g + f * h)

Equations

• Chapter9.Exercise_9_2_1d = sorry