Lean4
theorem isOpen_A_with_param {r s : ℝ} (hf : Continuous f.uncurry) (L : E →L[𝕜] F) :
IsOpen {p : α × E | p.2 ∈ A (f p.1) L r s} :=
by
have : ProperSpace E := .of_locallyCompactSpace 𝕜
simp only [A, mem_Ioc, mem_ball, map_sub, mem_setOf_eq]
apply isOpen_iff_mem_nhds.2
rintro ⟨a, x⟩ ⟨r', ⟨Irr', Ir'r⟩, hr⟩
rcases exists_between Irr' with ⟨t, hrt, htr'⟩
rcases exists_between hrt with ⟨t', hrt', ht't⟩
obtain ⟨b, b_lt, hb⟩ :
∃ b, b < s * r ∧ ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b :=
by
have B : Continuous (fun (p : E × E) ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) := by fun_prop
have C : (closedBall x t ×ˢ closedBall x t).Nonempty := by simp; linarith
rcases ((isCompact_closedBall x t).prod (isCompact_closedBall x t)).exists_isMaxOn C B.continuousOn with ⟨p, pt, hp⟩
simp only [mem_prod, mem_closedBall] at pt
refine
⟨‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖, hr p.1 (pt.1.trans_lt htr') p.2 (pt.2.trans_lt htr'), fun y hy z hz ↦ ?_⟩
have D : (y, z) ∈ closedBall x t ×ˢ closedBall x t := mem_prod.2 ⟨hy, hz⟩
exact hp D
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ b + 2 * ε < s * r := ⟨(s * r - b) / 3, by linarith, by linarith⟩
obtain ⟨u, u_open, au, hu⟩ :
∃ u,
IsOpen u ∧ a ∈ u ∧ ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (f.uncurry p) (f.uncurry (a, p.2)) < ε :=
by
have C : Continuous (fun (p : α × E) ↦ f a p.2) := by fun_prop
have D : ({ a } ×ˢ closedBall x t).EqOn f.uncurry (fun p ↦ f a p.2) :=
by
rintro ⟨b, y⟩ ⟨hb, -⟩
simp only [mem_singleton_iff] at hb
simp [hb]
obtain ⟨v, v_open, sub_v, hv⟩ :
∃ v, IsOpen v ∧ { a } ×ˢ closedBall x t ⊆ v ∧ ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε :=
Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq (s := { a } ×ˢ closedBall x t) (fun p _ ↦ hf.continuousAt)
(fun p _ ↦ C.continuousAt) D (dist_mem_uniformity εpos)
obtain ⟨w, w', w_open, -, sub_w, sub_w', hww'⟩ :
∃ (w : Set α) (w' : Set E), IsOpen w ∧ IsOpen w' ∧ { a } ⊆ w ∧ closedBall x t ⊆ w' ∧ w ×ˢ w' ⊆ v :=
generalized_tube_lemma isCompact_singleton (isCompact_closedBall x t) v_open sub_v
refine ⟨w, w_open, sub_w rfl, ?_⟩
rintro ⟨b, y⟩ h hby
exact hv _ (hww' ⟨h, sub_w' hby⟩)
have : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x) := prod_mem_nhds (u_open.mem_nhds au) (ball_mem_nhds _ (sub_pos.2 ht't))
filter_upwards [this]
rintro ⟨a', x'⟩ ha'x'
simp only [mem_prod, mem_ball] at ha'x'
refine ⟨t', ⟨hrt', ht't.le.trans (htr'.le.trans Ir'r)⟩, fun y hy z hz ↦ ?_⟩
have dyx : dist y x ≤ t := by linarith [dist_triangle y x' x]
have dzx : dist z x ≤ t := by linarith [dist_triangle z x' x]
calc
‖f a' z - f a' y - (L z - L y)‖ = ‖(f a' z - f a z) + (f a y - f a' y) + (f a z - f a y - (L z - L y))‖ := by congr;
abel
_ ≤ ‖f a' z - f a z‖ + ‖f a y - f a' y‖ + ‖f a z - f a y - (L z - L y)‖ := norm_add₃_le
_ ≤ ε + ε + b := by
gcongr
· rw [← dist_eq_norm]
change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
apply (hu _ _ _).le
· exact ha'x'.1
· simp [dzx]
· rw [← dist_eq_norm']
change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
apply (hu _ _ _).le
· exact ha'x'.1
· simp [dyx]
· simp [hb, dyx, dzx]
_ < s * r := by linarith
