X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
choose F hF_norm hF_dist using fun f : X →ᵇ ℝ => tietze_extension_step f e he
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
set g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - g.compContinuous e))^[n]) 0
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have g0 : g 0 = 0 := rfl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have g_succ : ∀ n, g (n + 1) = g n + F (f - (g n).compContinuous e) := fun n =>
  Function.iterate_succ_apply' _ _ _
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have hg_dist : ∀ n, dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n := by
  intro n
  calc
    dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
      rw [g_succ, dist_eq_norm', add_sub_cancel']
    _ ≤ ‖f - (g n).compContinuous e‖ / 3 := (hF_norm _)
    _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
    _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := (mul_le_mul_of_nonneg_left (hgf n) (by norm_num1))
    _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have hg_cau : CauchySeq g := cauchySeq_of_le_geometric _ _ (by norm_num1) hg_dist
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have :
  Tendsto (fun n => (g n).compContinuous e) atTop
    (𝓝 <| (limUnder atTop g).compContinuous e) :=
  ((continuous_compContinuous e).tendsto _).comp hg_cau.tendsto_limUnder
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
have hge : (limUnder atTop g).compContinuous e = f := by
  refine' tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 _)
  refine' squeeze_zero (fun _ => dist_nonneg) hgf _
  rw [← MulZeroClass.zero_mul ‖f‖]
  refine' (tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num1
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖limUnder atTop g‖ ≤ ‖f‖

case refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖f‖ ≤ ‖limUnder atTop g‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ compContinuous g e = f
refine' ⟨limUnder atTop g, le_antisymm _ _, hge⟩
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
⊢ dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
⊢ ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
intro n
case zero
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
⊢ dist (compContinuous (g Nat.zero) e) f ≤ (2 / 3) ^ Nat.zero * ‖f‖

case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist (compContinuous (g (Nat.succ n)) e) f ≤ (2 / 3) ^ Nat.succ n * ‖f‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
⊢ dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
induction' n with n ihn
no goals
case zero
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
⊢ dist (compContinuous (g Nat.zero) e) f ≤ (2 / 3) ^ Nat.zero * ‖f‖
simp [g0]
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist (compContinuous (F (f - compContinuous (g n) e)) e) (f - compContinuous (g n) e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist (compContinuous (g (Nat.succ n)) e) f ≤ (2 / 3) ^ Nat.succ n * ‖f‖
rw [g_succ n, add_compContinuous, ← dist_sub_right, add_sub_cancel', pow_succ, mul_assoc]
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ‖f - compContinuous (g n) e‖ ≤ (2 / 3) ^ n * ‖f‖
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist (compContinuous (F (f - compContinuous (g n) e)) e) (f - compContinuous (g n) e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)
refine' (hF_dist _).trans (mul_le_mul_of_nonneg_left _ (by norm_num1))
no goals
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ‖f - compContinuous (g n) e‖ ≤ (2 / 3) ^ n * ‖f‖
rwa [← dist_eq_norm']
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
n : ℕ
ihn : dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ 0 ≤ 2 / 3
norm_num1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
intro n
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
calc
  dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
    rw [g_succ, dist_eq_norm', add_sub_cancel']
  _ ≤ ‖f - (g n).compContinuous e‖ / 3 := (hF_norm _)
  _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
  _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := (mul_le_mul_of_nonneg_left (hgf n) (by norm_num1))
  _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g (n + 1)) = ‖F (f - compContinuous (g n) e)‖
rw [g_succ, dist_eq_norm', add_sub_cancel']
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ ‖f - compContinuous (g n) e‖ / 3 = 1 / 3 * dist (compContinuous (g n) e) f
rw [dist_eq_norm', one_div, div_eq_inv_mul]
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ 0 ≤ 1 / 3
norm_num1
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ 1 / 3 * ((2 / 3) ^ n * ‖f‖) = 1 / 3 * ‖f‖ * (2 / 3) ^ n
ac_rfl
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ 2 / 3 < 1
norm_num1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun b => dist (compContinuous (g b) e) f) atTop (𝓝 0)
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ compContinuous (limUnder atTop g) e = f
refine' tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 _)
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun t => (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun b => dist (compContinuous (g b) e) f) atTop (𝓝 0)
refine' squeeze_zero (fun _ => dist_nonneg) hgf _
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun t => (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun t => (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)
rw [← MulZeroClass.zero_mul ‖f‖]
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
⊢ Tendsto (fun t => (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))
refine' (tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num1
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ dist (g 0) (limUnder atTop g) ≤ ‖f‖
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖limUnder atTop g‖ ≤ ‖f‖
rw [← dist_zero_left, ← g0]
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ 1 / 3 * ‖f‖ / (1 - 2 / 3) = ‖f‖
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ dist (g 0) (limUnder atTop g) ≤ ‖f‖
refine'
  (dist_le_of_le_geometric_of_tendsto₀ _ _ (by norm_num1)
    hg_dist hg_cau.tendsto_limUnder).trans_eq _
no goals
case refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ 1 / 3 * ‖f‖ / (1 - 2 / 3) = ‖f‖
field_simp [show (3 - 2 : ℝ) = 1 by norm_num1]
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ 2 / 3 < 1
norm_num1
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ 3 - 2 = 1
norm_num1
case refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖compContinuous (limUnder atTop g) e‖ ≤ ‖limUnder atTop g‖
case refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖f‖ ≤ ‖limUnder atTop g‖
rw [← hge]
no goals
case refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist (compContinuous (F f) e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n => ((fun g => g + F (f - compContinuous g e))^[n]) 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - compContinuous (g n) e)
hgf : ∀ (n : ℕ), dist (compContinuous (g n) e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n => compContinuous (g n) e) atTop (𝓝 (compContinuous (limUnder atTop g) e))
hge : compContinuous (limUnder atTop g) e = f
⊢ ‖compContinuous (limUnder atTop g) e‖ ≤ ‖limUnder atTop g‖
exact norm_compContinuous_le _ _