bookshelf/Common/Real/Function/Step.lean

67 lines
2.0 KiB
Plaintext
Raw Normal View History

2023-05-08 19:37:02 +00:00
import Common.Real.Basic
import Common.Real.Set.Partition
2023-05-08 19:37:02 +00:00
/-! # Common.Real.Function.Step
2023-05-04 22:37:54 +00:00
A characterization of step functions.
-/
namespace Real.Function
2023-04-24 18:59:11 +00:00
open Partition
/--
Any member of a subinterval of a partition `P` must also be a member of `P`.
-/
lemma mem_open_subinterval_imp_mem_partition {p : Partition}
(hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂))
(hy : y ∈ I) : y ∈ p := by
2023-04-24 18:59:11 +00:00
cases h : p.xs with
2023-04-28 13:35:58 +00:00
| nil =>
-- By definition, a partition must always have at least two points in the
-- interval. Discharge the empty case.
rw [h] at hI
cases hI
2023-04-24 18:59:11 +00:00
| cons x ys =>
2023-04-28 13:35:58 +00:00
have ⟨i, x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩ :=
List.mem_pairwise_imp_exists_adjacent hI
have hx₁ : x₁ ∈ p.xs := by
rw [hx₁]
let j : Fin (List.length p.xs) := ⟨i.1, Nat.lt_of_lt_pred i.2⟩
exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩
have hx₂ : x₂ ∈ p.xs := by
rw [hx₂]
let j : Fin (List.length p.xs) := ⟨i.1 + 1, lt_tsub_iff_right.mp i.2⟩
exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩
2023-04-24 18:59:11 +00:00
rw [hI'] at hy
2023-04-28 13:35:58 +00:00
apply And.intro
2023-04-24 18:59:11 +00:00
· calc p.left
_ ≤ x₁ := (subdivision_point_mem_partition hx₁).left
_ ≤ y := le_of_lt hy.left
· calc y
_ ≤ x₂ := le_of_lt hy.right
_ ≤ p.right := (subdivision_point_mem_partition hx₂).right
/--
2023-04-24 18:59:11 +00:00
A function `f` is a `Step` function if there exists a `Partition` `p` such that
`f` is constant on every open subinterval of `p`.
-/
structure Step where
p : Partition
f : ∀ x ∈ p,
const_open_subintervals :
∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂)),
∃ c : , ∀ (hy : y ∈ I),
f y (mem_open_subinterval_imp_mem_partition hI hy) = c
namespace Step
2023-04-24 18:59:11 +00:00
/--
The set definition of a `Step` function is the region between the constant
values of the function's subintervals and the real axis.
-/
def set_def (f : Step) : Set ℝ² := sorry
2023-04-24 18:59:11 +00:00
end Step
2023-04-24 18:59:11 +00:00
end Real.Function