Аналіз I, Розділ 11.2: Кусочно-постійні функції

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

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

Кусочно-постійні функції.
Інтеграл кусочно-постійної функції.

namespace Chapter11open BoundedInterval

Визначення 11.2.1

abbrev Constant {X Y:Type} (f: X → Y) : Prop := ∃ c, ∀ x, f x = c

open Classical in
noncomputable abbrev constant_value {X Y:Type} [hY: Nonempty Y] (f:X → Y) : Y :=
  if h: Constant f then h.choose else hY.some

theorem Constant.eq {X Y:Type} {f: X → Y} [Nonempty Y] (h: Constant f) (x:X) :
  f x = constant_value f := byX:TypeY:Typef:X → Yinst✝:Nonempty Yh:Constant fx:X⊢ f x = constant_value f simp [constant_value, h]X:TypeY:Typef:X → Yinst✝:Nonempty Yh:Constant fx:X⊢ f x = Exists.choose ⋯; apply h.choose_specAll goals completed! 🐙

theorem Constant.of_const {X Y:Type} {f:X → Y} {c:Y} (h: ∀ x, f x = c) :
  Constant f := byX:TypeY:Typef:X → Yc:Yh:∀ (x : X), f x = c⊢ Constant f use cAll goals completed! 🐙

theorem Constant.const_eq {X Y:Type} {f:X → Y} [hX: Nonempty X] [Nonempty Y] {c:Y} (h: ∀ x, f x = c) :
  constant_value f = c := byX:TypeY:Typef:X → YhX:Nonempty Xinst✝:Nonempty Yc:Yh:∀ (x : X), f x = c⊢ constant_value f = c rw [←eq (of_const h) hX.some, h hX.some]All goals completed! 🐙

theorem Constant.of_subsingleton {X Y:Type} [hs: Subsingleton X] [hY: Nonempty Y] {f:X → Y} :
  Constant f := byX:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Y⊢ Constant f
  by_cases h:Nonempty Xpos._@._hyg.233X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ Constant fneg._@._hyg.233X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:¬Nonempty X⊢ Constant f
  .pos._@._hyg.233X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ Constant f use f h.somehX:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ ∀ (x : X), f x = f h.some; introshX:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty Xx✝:X⊢ f x✝ = f h.some; congrh.e_aX:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty Xx✝:X⊢ x✝ = h.some; exact hs.elim _ h.someAll goals completed! 🐙
  simp at hneg._@._hyg.233X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:IsEmpty X⊢ Constant f; exact ⟨ hY.some, h.elim ⟩All goals completed! 🐙

abbrev ConstantOn (f: ℝ → ℝ) (X: Set ℝ) : Prop := Constant (fun x : X ↦ f ↑x)noncomputable abbrev constant_value_on (f:ℝ → ℝ) (X: Set ℝ) : ℝ := constant_value (fun x : X ↦ f ↑x)

theorem ConstantOn.eq {f: ℝ → ℝ} {X: Set ℝ} (h: ConstantOn f X) {x:ℝ} (hx: x ∈ X) :
  f x = constant_value_on f X := byf:ℝ → ℝX:Set ℝh:ConstantOn f Xx:ℝhx:x ∈ X⊢ f x = constant_value_on f X
  convert Constant.eq h ⟨ _, hx ⟩All goals completed! 🐙

theorem ConstantOn.of_const {f:ℝ → ℝ} {X: Set ℝ} {c:ℝ} (h: ∀ x ∈ X, f x = c) :
  ConstantOn f X := ⟨ c, byf:ℝ → ℝX:Set ℝc:ℝh:∀ x ∈ X, f x = c⊢ ∀ (x : ↑X), (fun x => f ↑x) x = c grindAll goals completed! 🐙 ⟩

theorem ConstantOn.of_const' (c:ℝ) (X:Set ℝ): ConstantOn (fun _ ↦ c) X := of_const (c := c) (byc:ℝX:Set ℝ⊢ ∀ x ∈ X, c = c simpAll goals completed! 🐙)

theorem ConstantOn.const_eq {f:ℝ → ℝ} {X: Set ℝ} (hX: X.Nonempty) {c:ℝ} (h: ∀ x ∈ X, f x = c) :
  constant_value_on f X = c := byf:ℝ → ℝX:Set ℝhX:X.Nonemptyc:ℝh:∀ x ∈ X, f x = c⊢ constant_value_on f X = c
    rw [←eq (of_const h) hX.some_mem, h _ hX.some_mem]All goals completed! 🐙

theorem ConstantOn.congr {f g: ℝ → ℝ} {X: Set ℝ} (h: ∀ x ∈ X, f x = g x) : ConstantOn f X ↔ ConstantOn g X := byf:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ ConstantOn f X ↔ ConstantOn g X
  simp_rw [ConstantOn, iff_iff_eq]f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (Constant fun x => f ↑x) = Constant fun x => g ↑x; congre_ff:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (fun x => f ↑x) = fun x => g ↑x; grindAll goals completed! 🐙

theorem ConstantOn.congr' {f g: ℝ → ℝ} {X: Set ℝ} (hf: ConstantOn f X) (h: ∀ x ∈ X, f x = g x) : ConstantOn g X := (congr h).mp hf

theorem ConstantOn.of_subsingleton {f: ℝ → ℝ} {X: Set ℝ} [Subsingleton X] :
  ConstantOn f X := Constant.of_subsingleton

theorem constant_value_on_congr {f g: ℝ → ℝ} {X: Set ℝ} (h: ∀ x ∈ X, f x = g x) :
  constant_value_on f X = constant_value_on g X := byf:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ constant_value_on f X = constant_value_on g X
  simp [constant_value_on]f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (constant_value fun x => f ↑x) = constant_value fun x => g ↑x; congre_ff:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (fun x => f ↑x) = fun x => g ↑x; grindAll goals completed! 🐙

Визначення 11.2.3 (Кусочно-постійні функції I)

abbrev PiecewiseConstantWith (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : Prop := ∀ J ∈ P, ConstantOn f (J:Set ℝ)

theorem PiecewiseConstantWith.def (f:ℝ → ℝ) {I: BoundedInterval} {P: Partition I} :
  PiecewiseConstantWith f P ↔ ∀ J ∈ P, ∃ c, ∀ x ∈ J, f x = c := byf:ℝ → ℝI:BoundedIntervalP:Partition I⊢ PiecewiseConstantWith f P ↔ ∀ J ∈ P, ∃ c, ∀ x ∈ J, f x = c
    simp [PiecewiseConstantWith, ConstantOn, Constant, mem_iff]All goals completed! 🐙

theorem PiecewiseConstantWith.congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
  (h: ∀ x ∈ (I:Set ℝ), f x = g x) :
  PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P
  simp [PiecewiseConstantWith]f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ (∀ J ∈ P, ConstantOn f ↑J) ↔ ∀ J ∈ P, ConstantOn g ↑J; peel with J hJh.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P⊢ ConstantOn f ↑J ↔ ConstantOn g ↑J
  apply ConstantOn.congrh.h.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P⊢ ∀ x ∈ ↑J, f x = g x; have := P.contains _ hJh.h.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ Pthis:?_mvar.35023 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ x ∈ ↑J, f x = g x; grind [subset_iff]All goals completed! 🐙

Визначення 11.2.5 (Кусочно-постійні функції I)

abbrev PiecewiseConstantOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop := ∃ P : Partition I, PiecewiseConstantWith f P

theorem PiecewiseConstantOn.def (f:ℝ → ℝ) (I: BoundedInterval):
  PiecewiseConstantOn f I ↔ ∃ P : Partition I, ∀ J ∈ P, ConstantOn f (J:Set ℝ) := byf:ℝ → ℝI:BoundedInterval⊢ PiecewiseConstantOn f I ↔ ∃ P, ∀ J ∈ P, ConstantOn f ↑J rflAll goals completed! 🐙

theorem PiecewiseConstantOn.congr {f g: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), f x = g x) :
  PiecewiseConstantOn f I ↔ PiecewiseConstantOn g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g x⊢ PiecewiseConstantOn f I ↔ PiecewiseConstantOn g I
  simp_rw [PiecewiseConstantOn, PiecewiseConstantWith.congr h]All goals completed! 🐙

theorem PiecewiseConstantOn.congr' {f g: ℝ → ℝ} {I: BoundedInterval} (hf: PiecewiseConstantOn f I) (h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantOn g I := (congr h).mp hf

Приклад 11.2.4 / Приклад 11.2.6

noncomputable abbrev f_11_2_4 : ℝ → ℝ := fun x ↦
  if x < 1 then 0 else  -- сміттеве значення
    if x < 3 then 7 else
      if x = 3 then 4 else
        if x < 6 then 5 else
          if x = 6 then 2 else
            0 -- сміттеве значення

declaration uses 'sorry'example : PiecewiseConstantOn f_11_2_4 (Icc 1 6) := by⊢ PiecewiseConstantOn f_11_2_4 (Icc 1 6)
  use Partition.mk { Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6} ?_ ?_h⊢ PiecewiseConstantWith f_11_2_4
  { intervals := {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, exists_unique := ?w.refine_1, contains := ?w.refine_2 }w.refine_1⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6} ∧ x ∈ Jw.refine_2⊢ ∀ J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, J ⊆ Icc 1 6
  .h⊢ PiecewiseConstantWith f_11_2_4
  { intervals := {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, exists_unique := ?w.refine_1, contains := ?w.refine_2 } sorryAll goals completed! 🐙
  .w.refine_1⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6} ∧ x ∈ J sorryAll goals completed! 🐙
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : PiecewiseConstantOn f_11_2_4 (Icc 1 6) := by⊢ PiecewiseConstantOn f_11_2_4 (Icc 1 6)
  use Partition.mk { Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6} ?_ ?_h⊢ PiecewiseConstantWith f_11_2_4
  { intervals := {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, exists_unique := ?w.refine_1,
    contains := ?w.refine_2 }w.refine_1⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6} ∧ x ∈ Jw.refine_2⊢ ∀ J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, J ⊆ Icc 1 6
  .h⊢ PiecewiseConstantWith f_11_2_4
  { intervals := {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, exists_unique := ?w.refine_1,
    contains := ?w.refine_2 } sorryAll goals completed! 🐙
  .w.refine_1⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6} ∧ x ∈ J sorryAll goals completed! 🐙
  sorryAll goals completed! 🐙

Приклад 11.2.6

theorem declaration uses 'sorry'ConstantOn.piecewiseConstantOn {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
  PiecewiseConstantOn f I := byf:ℝ → ℝI:BoundedIntervalh:ConstantOn f ↑I⊢ PiecewiseConstantOn f I sorryAll goals completed! 🐙

Лема 11.2.7 / Вправа 11.2.1

theorem declaration uses 'sorry'PiecewiseConstantWith.mono {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I} (hPP': P ≤ P')
  (hP: PiecewiseConstantWith f P) : PiecewiseConstantWith f P' := byf:ℝ → ℝI:BoundedIntervalP:Partition IP':Partition IhPP':P ≤ P'hP:PiecewiseConstantWith f P⊢ PiecewiseConstantWith f P'
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.add {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f + g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f + g) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.sub {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f - g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f - g) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.max {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (max f g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f ⊔ g) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.min {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (min f g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f ⊓ g) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.mul {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f * g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f * g) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2

theorem declaration uses 'sorry'PiecewiseConstantOn.smul {f: ℝ → ℝ} {I: BoundedInterval}
  (c:ℝ) (hf: PiecewiseConstantOn f I) : PiecewiseConstantOn (c • f) I := byf:ℝ → ℝI:BoundedIntervalc:ℝhf:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (c • f) I
  sorryAll goals completed! 🐙

Лема 11.2.8 / Вправа 11.2.2. Вважаю, що гіпотеза про те, що Unknown identifier `g`g не дорівнює нулю, не потрібна.

theorem declaration uses 'sorry'PiecewiseConstantOn.div {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn f I) : PiecewiseConstantOn (f / g) I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (f / g) I
  sorryAll goals completed! 🐙

Визначення 11.2.9 (Інтеграл кусочно-постійної функції I)

noncomputable abbrev PiecewiseConstantWith.integ (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I)  :
  ℝ := ∑ J ∈ P.intervals, constant_value_on f (J:Set ℝ) * |J|ₗ

theorem PiecewiseConstantWith.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f P = integ g P := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ integ f P = integ g P
  apply Finset.sum_congr rflf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ ∀ x ∈ P.intervals, constant_value_on f ↑x * x.length = constant_value_on g ↑x * x.length; intro J hJf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * J.length = constant_value_on g ↑J * J.length; congr 1e_a._@.Init.Prelude._hyg.2164f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J = constant_value_on g ↑J; apply constant_value_on_congre_a.h._@.Init.Prelude._hyg.2164f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ ∀ x ∈ ↑J, f x = g x
  have := P.contains _ hJe_a.h._@.Init.Prelude._hyg.2164f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervalsthis:?_mvar.39776 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ x ∈ ↑J, f x = g x; grind [subset_iff]All goals completed! 🐙

Приклад 11.2.12

noncomputable abbrev f_11_2_12 : ℝ → ℝ := fun x ↦
    if x < 3 then 2 else
      if x = 3 then 4 else
        6

noncomputable abbrev P_11_2_12 : Partition (Icc 1 4) :=
  ((⊥: Partition (Ico 1 3)).join (⊥ : Partition (Icc 3 3))
  (join_Ico_Icc (by⊢ 1 ≤ 3 norm_numAll goals completed! 🐙) (by⊢ 3 ≤ 3 norm_numAll goals completed! 🐙) )).join
  (⊥: Partition (Ioc 3 4))
  (join_Icc_Ioc (by⊢ 1 ≤ 3 norm_numAll goals completed! 🐙) (by⊢ 3 ≤ 4 norm_numAll goals completed! 🐙))

declaration uses 'sorry'example : PiecewiseConstantWith f_11_2_12 P_11_2_12 := by⊢ PiecewiseConstantWith f_11_2_12 P_11_2_12
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : PiecewiseConstantWith.integ f_11_2_12 P_11_2_12 = 10 := by⊢ PiecewiseConstantWith.integ f_11_2_12 P_11_2_12 = 10
  sorryAll goals completed! 🐙

noncomputable abbrev P_11_2_12' : Partition (Icc 1 4) :=
  ((((⊥: Partition (Ico 1 2)).join (⊥ : Partition (Ico 2 3))
  (join_Ico_Ico (by⊢ 1 ≤ 2 norm_numAll goals completed! 🐙) (by⊢ 2 ≤ 3 norm_numAll goals completed! 🐙) )).join
  (⊥: Partition (Icc 3 3))
  (join_Ico_Icc (by⊢ 1 ≤ 3 norm_numAll goals completed! 🐙) (by⊢ 3 ≤ 3 norm_numAll goals completed! 🐙))).join
  (⊥: Partition (Ioc 3 4))
  (join_Icc_Ioc (by⊢ 1 ≤ 3 norm_numAll goals completed! 🐙) (by⊢ 3 ≤ 4 norm_numAll goals completed! 🐙))).add_empty

declaration uses 'sorry'example : PiecewiseConstantWith f_11_2_12 P_11_2_12' := by⊢ PiecewiseConstantWith f_11_2_12 P_11_2_12'
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : PiecewiseConstantWith.integ f_11_2_12 P_11_2_12' = 10 := by⊢ PiecewiseConstantWith.integ f_11_2_12 P_11_2_12' = 10
  sorryAll goals completed! 🐙

Твердження 11.2.13 (Інтеграл кусочно-постійної функції не залежить від розбиття) / Вправа 11.2.3

theorem declaration uses 'sorry'PiecewiseConstantWith.integ_eq {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I}
  (hP: PiecewiseConstantWith f P) (hP': PiecewiseConstantWith f P') : integ f P = integ f P' := byf:ℝ → ℝI:BoundedIntervalP:Partition IP':Partition IhP:PiecewiseConstantWith f PhP':PiecewiseConstantWith f P'⊢ integ f P = integ f P'
  sorryAll goals completed! 🐙

open Classical in
/-- Визначення 11.2.14 (Інтеграл кусочно-постійної функції II)  -/
noncomputable abbrev PiecewiseConstantOn.integ (f:ℝ → ℝ) (I: BoundedInterval) :
  ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.integ f h.choose else 0

noncomputable abbrev PiecewiseConstantOn.integ' {f:ℝ → ℝ} {I: BoundedInterval} (_:PiecewiseConstantOn f I) := integ f I

theorem PiecewiseConstantOn.integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
  (h: PiecewiseConstantWith f P) : integ f I = PiecewiseConstantWith.integ f P := byf:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f P⊢ integ f I = PiecewiseConstantWith.integ f P
  have h' : PiecewiseConstantOn f I := byf:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f P⊢ integ f I = PiecewiseConstantWith.integ f P use PAll goals completed! 🐙
  simp [integ, h']f:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f Ph':Chapter11.PiecewiseConstantOn _fvar.43611 _fvar.43612 := ?_mvar.43620⊢ PiecewiseConstantWith.integ f (Exists.choose ⋯) = PiecewiseConstantWith.integ f P; exact PiecewiseConstantWith.integ_eq h'.choose_spec hAll goals completed! 🐙

theorem PiecewiseConstantOn.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval}
  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f I = integ g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g x⊢ integ f I = integ g I
  by_cases hf : PiecewiseConstantOn f Ipos._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f I⊢ integ f I = integ g Ineg._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f I⊢ integ f I = integ g I
  <;>pos._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f I⊢ integ f I = integ g Ineg._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f I⊢ integ f I = integ g I (have hg := hfneg._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f Ihg:?_mvar.48511 := _fvar.46959⊢ integ f I = integ g I; rw [congr h] at hgneg._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f Ihg:¬PiecewiseConstantOn g I⊢ integ f I = integ g I; simp [integ, hf, hg]All goals completed! 🐙)
  rw [PiecewiseConstantWith.integ_congr h, ←integ_def hg.choose_spec, ←integ_def]pos._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantWith g (Exists.choose ⋯)
  rw [←PiecewiseConstantWith.congr h]pos._@._hyg.2620f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantWith f (Exists.choose ⋯); exact hf.choose_specAll goals completed! 🐙

Приклад 11.2.15

declaration uses 'sorry'example : PiecewiseConstantOn.integ f_11_2_4 (Icc 1 6) = 10 := by⊢ PiecewiseConstantOn.integ f_11_2_4 (Icc 1 6) = 10
  sorryAll goals completed! 🐙

Теорема 11.2.16 (a) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_add {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
  integ (f + g) I = integ f I + integ g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ (f + g) I = integ f I + integ g I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (b) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ) (hf: PiecewiseConstantOn f I) :
  integ (c • f) I = c * integ f I
   := byf:ℝ → ℝI:BoundedIntervalc:ℝhf:PiecewiseConstantOn f I⊢ integ (c • f) I = c * integ f I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (c) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_sub {f g: ℝ → ℝ} {I: BoundedInterval}
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
  integ (f - g) I = integ f I - integ g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ (f - g) I = integ f I - integ g I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (d) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_of_nonneg {f: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ I, 0 ≤ f x)
  (hf: PiecewiseConstantOn f I) :
  0 ≤ integ f I := byf:ℝ → ℝI:BoundedIntervalh:∀ x ∈ I, 0 ≤ f xhf:PiecewiseConstantOn f I⊢ 0 ≤ integ f I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (e) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_mono {f g: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ I, f x ≤ g x)
  (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
  integ f I ≤ integ g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ I, f x ≤ g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ f I ≤ integ g I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (f) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_const (c: ℝ) (I: BoundedInterval) :
  integ (fun _ ↦ c) I = c * |I|ₗ := byc:ℝI:BoundedInterval⊢ integ (fun x => c) I = c * I.length
  sorryAll goals completed! 🐙

Теорема 11.2.16 (f) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_const' {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f I) :
  integ f I = (constant_value_on f I) * |I|ₗ := byf:ℝ → ℝI:BoundedIntervalh:ConstantOn f ↑I⊢ integ f I = constant_value_on f ↑I * I.length
  sorryAll goals completed! 🐙

open Classical in
/-- Теорема 11.2.16 (g) (Закони інтегрування) / Вправа 11.2.4 -/
theorem declaration uses 'sorry'PiecewiseConstantOn.of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
  {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) :
  PiecewiseConstantOn (fun x ↦ if x ∈ I then f x else 0) J := byI:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (fun x => if x ∈ I then f x else 0) J
  sorryAll goals completed! 🐙

open Classical in
/-- Теорема 11.2.16 (g) (Закони інтегрування) / Вправа 11.2.4 -/
theorem declaration uses 'sorry'PiecewiseConstantOn.integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
  {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) :
  integ (fun x ↦ if x ∈ I then f x else 0) J = integ f I := byI:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f I⊢ integ (fun x => if x ∈ I then f x else 0) J = integ f I
  sorryAll goals completed! 🐙

Теорема 11.2.16 (h) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.of_join {I J K: BoundedInterval} (hIJK: K.joins I J)
  (f: ℝ → ℝ) : PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J := byI:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJK:K.joins I Jf:ℝ → ℝ⊢ PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J
  sorryAll goals completed! 🐙

Теорема 11.2.16 (h) (Закони інтегрування) / Вправа 11.2.4

theorem declaration uses 'sorry'PiecewiseConstantOn.integ_of_join {I J K: BoundedInterval} (hIJK: K.joins I J)
  {f: ℝ → ℝ} (h: PiecewiseConstantOn f K) :
  integ f K = integ f I + integ f J := byI:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJK:K.joins I Jf:ℝ → ℝh:PiecewiseConstantOn f K⊢ integ f K = integ f I + integ f J
  sorryAll goals completed! 🐙

end Chapter11