English
If K is complete, then D(f,K) equals the set {x ∈ R | DifferentiableWithinAt f (Ici x) x and derivWithin f (Ici x) x ∈ K}.
Русский
Если K полное, то D(f,K) равно множеству {x ∈ R | DifferentiableWithinAt f (Ici x) x и derivWithin f (Ici x) x ∈ K}.
LaTeX
$$D f K = \\{ x ∈ \\mathbb{R} \\mid \\text{DifferentiableWithinAt } \\mathbb{R} f (Ici x) x \\land \\ derivWithin f (Ici x) x ∈ K \\} (при K полном)$$
Lean4
/-- Harder inclusion: at a point in `D f K`, the function `f` has a derivative, in `K`. -/
theorem D_subset_differentiable_set {K : Set F} (hK : IsComplete K) :
D f K ⊆ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} :=
by
have P : ∀ {n : ℕ}, (0 : ℝ) < (1 / 2) ^ n := fun {n} => pow_pos (by norm_num) n
intro x hx
have :
∀ e : ℕ,
∃ n : ℕ,
∀ p q, n ≤ p → n ≤ q → ∃ L ∈ K, x ∈ A f L ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f L ((1 / 2) ^ q) ((1 / 2) ^ e) :=
by
intro e
have := mem_iInter.1 hx e
rcases mem_iUnion.1 this with ⟨n, hn⟩
refine ⟨n, fun p q hp hq => ?_⟩
simp only [mem_iInter] at hn
rcases mem_iUnion.1 (hn p hp q hq) with ⟨L, hL⟩
exact
⟨L, exists_prop.mp <| mem_iUnion.1 hL⟩
/- Recast the assumptions: for each `e`, there exist `n e` and linear maps `L e p q` in `K`
such that, for `p, q ≥ n e`, then `f` is well approximated by `L e p q` at scale `2 ^ (-p)` and
`2 ^ (-q)`, with an error `2 ^ (-e)`. -/
choose! n L hn using this
have M :
∀ e p q e' p' q', n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e :=
by
intro e p q e' p' q' hp hq hp' hq' he'
let r := max (n e) (n e')
have I : ((1 : ℝ) / 2) ^ e' ≤ (1 / 2) ^ e := pow_le_pow_of_le_one (by norm_num) (by norm_num) he'
have J1 : ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e :=
by
have I1 : x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p q hp hq).2.1
have I2 : x ∈ A f (L e p r) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.1
exact norm_sub_le_of_mem_A P _ I1 I2
have J2 : ‖L e p r - L e' p' r‖ ≤ 4 * (1 / 2) ^ e :=
by
have I1 : x ∈ A f (L e p r) ((1 / 2) ^ r) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.2
have I2 : x ∈ A f (L e' p' r) ((1 / 2) ^ r) ((1 / 2) ^ e') := (hn e' p' r hp' (le_max_right _ _)).2.2
exact norm_sub_le_of_mem_A P _ I1 (A_mono _ _ I I2)
have J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e :=
by
have I1 : x ∈ A f (L e' p' r) ((1 / 2) ^ p') ((1 / 2) ^ e') := (hn e' p' r hp' (le_max_right _ _)).2.1
have I2 : x ∈ A f (L e' p' q') ((1 / 2) ^ p') ((1 / 2) ^ e') := (hn e' p' q' hp' hq').2.1
exact norm_sub_le_of_mem_A P _ (A_mono _ _ I I1) (A_mono _ _ I I2)
calc
‖L e p q - L e' p' q'‖ = ‖L e p q - L e p r + (L e p r - L e' p' r) + (L e' p' r - L e' p' q')‖ := by congr 1;
abel
_ ≤ ‖L e p q - L e p r‖ + ‖L e p r - L e' p' r‖ + ‖L e' p' r - L e' p' q'‖ :=
(le_trans (norm_add_le _ _) (add_le_add_right (norm_add_le _ _) _))
_ ≤ 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e := by gcongr
_ = 12 * (1 / 2) ^ e := by
ring
/- For definiteness, use `L0 e = L e (n e) (n e)`, to have a single sequence. We claim that this
is a Cauchy sequence. -/
let L0 : ℕ → F := fun e => L e (n e) (n e)
have : CauchySeq L0 := by
rw [Metric.cauchySeq_iff']
intro ε εpos
obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / 12 := exists_pow_lt_of_lt_one (div_pos εpos (by norm_num)) (by norm_num)
refine ⟨e, fun e' he' => ?_⟩
rw [dist_comm, dist_eq_norm]
calc
‖L0 e - L0 e'‖ ≤ 12 * (1 / 2) ^ e := M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
_ < 12 * (ε / 12) := (mul_lt_mul' le_rfl he (le_of_lt P) (by norm_num))
_ = ε := by
field_simp
-- As it is Cauchy, the sequence `L0` converges, to a limit `f'` in `K`.
obtain ⟨f', f'K, hf'⟩ : ∃ f' ∈ K, Tendsto L0 atTop (𝓝 f') :=
cauchySeq_tendsto_of_isComplete hK (fun e => (hn e (n e) (n e) le_rfl le_rfl).1) this
have Lf' : ∀ e p, n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e :=
by
intro e p hp
apply le_of_tendsto (tendsto_const_nhds.sub hf').norm
rw [eventually_atTop]
exact
⟨e, fun e' he' => M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩
-- Let us show that `f` has right derivative `f'` at `x`.
have : HasDerivWithinAt f f' (Ici x) x :=
by
simp only [hasDerivWithinAt_iff_isLittleO, isLittleO_iff]
/- to get an approximation with a precision `ε`, we will replace `f` with `L e (n e) m` for
some large enough `e` (yielding a small error by uniform approximation). As one can vary `m`,
this makes it possible to cover all scales, and thus to obtain a good linear approximation in
the whole interval of length `(1/2)^(n e)`. -/
intro ε εpos
obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / 16 := exists_pow_lt_of_lt_one (div_pos εpos (by norm_num)) (by norm_num)
filter_upwards [Icc_mem_nhdsGE <| show x < x + (1 / 2) ^ (n e + 1) by simp] with y hy
rcases eq_or_lt_of_le hy.1 with (rfl | xy)
· simp only [sub_self, zero_smul, norm_zero, mul_zero, le_rfl]
have yzero : 0 < y - x := sub_pos.2 xy
have y_le : y - x ≤ (1 / 2) ^ (n e + 1) := by linarith [hy.2]
have yone : y - x ≤ 1 :=
le_trans y_le
(pow_le_one₀ (by norm_num) (by norm_num))
-- define the scale `k`.
obtain ⟨k, hk, h'k⟩ : ∃ k : ℕ, (1 / 2) ^ (k + 1) < y - x ∧ y - x ≤ (1 / 2) ^ k :=
exists_nat_pow_near_of_lt_one yzero yone (by norm_num : (0 : ℝ) < 1 / 2)
(by norm_num : (1 : ℝ) / 2 < 1)
-- the scale is large enough (as `y - x` is small enough)
have k_gt : n e < k :=
by
have : ((1 : ℝ) / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1) := lt_of_lt_of_le hk y_le
rw [pow_lt_pow_iff_right_of_lt_one₀ (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)] at this
omega
set m := k - 1
have m_ge : n e ≤ m := Nat.le_sub_one_of_lt k_gt
have km : k = m + 1 := (Nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) k_gt)).symm
rw [km] at hk h'k
have J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖ :=
calc
‖f y - f x - (y - x) • L e (n e) m‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m :=
by
apply le_of_mem_A (hn e (n e) m le_rfl m_ge).2.2
· simp only [one_div, inv_pow, left_mem_Icc, le_add_iff_nonneg_right]
positivity
· simp only [pow_add, tsub_le_iff_left] at h'k
simpa only [hy.1, mem_Icc, true_and, one_div, pow_one] using h'k
_ = 4 * (1 / 2) ^ e * (1 / 2) ^ (m + 2) := by field_simp; ring
_ ≤ 4 * (1 / 2) ^ e * (y - x) := by gcongr
_ = 4 * (1 / 2) ^ e * ‖y - x‖ := by rw [Real.norm_of_nonneg yzero.le]
calc
‖f y - f x - (y - x) • f'‖ = ‖f y - f x - (y - x) • L e (n e) m + (y - x) • (L e (n e) m - f')‖ := by
simp only [smul_sub, sub_add_sub_cancel]
_ ≤ 4 * (1 / 2) ^ e * ‖y - x‖ + ‖y - x‖ * (12 * (1 / 2) ^ e) :=
(norm_add_le_of_le J <| by rw [norm_smul]; gcongr; exact Lf' _ _ m_ge)
_ = 16 * ‖y - x‖ * (1 / 2) ^ e := by ring
_ ≤ 16 * ‖y - x‖ * (ε / 16) := by gcongr
_ = ε * ‖y - x‖ := by
ring
-- Conclusion of the proof
rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.left_mem_Ici)] at f'K
exact ⟨this.differentiableWithinAt, f'K⟩
