English
A variant of tendsto_concat asserting identity of limit components under compatible endpoint behavior in the same framework as 202274.
Русский
вариант tendsto_concat, указывающий на идентичность пределов компонентов при согласованной конечной поведении.
LaTeX
$$tendsto_concat_variant: under compatible endpoint behavior, concatenation tends to concatenation.$$
Lean4
theorem tendsto_concat {ι : Type*} {p : Filter ι} {F : ι → C(Icc a b, E)} {G : ι → C(Icc b c, E)}
(hfg : ∀ᶠ i in p, (F i) ⊤ = (G i) ⊥) (hfg' : f ⊤ = g ⊥) (hf : Tendsto F p (𝓝 f)) (hg : Tendsto G p (𝓝 g)) :
Tendsto (fun i => concat (F i) (G i)) p (𝓝 (concat f g)) :=
by
rw [tendsto_nhds_compactOpen] at hf hg ⊢
rintro K hK U hU hfgU
have h : b ∈ Icc a c := ⟨Fact.out, Fact.out⟩
let K₁ : Set (Icc a b) := projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
let K₂ : Set (Icc b c) := projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
have hK₁ : IsCompact K₁ := hK.inter_right isClosed_Iic |>.image continuous_subtype_val |>.image projIccCM.continuous
have hK₂ : IsCompact K₂ := hK.inter_right isClosed_Ici |>.image continuous_subtype_val |>.image projIccCM.continuous
have hfU : MapsTo f K₁ U := by
rw [← concat_comp_IccInclusionLeft hfg']
apply hfgU.comp
rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : z ≤ b)⟩, rfl⟩, rfl⟩
simpa [projIccCM, projIcc, h2, hz.1] using h1
have hgU : MapsTo g K₂ U := by
rw [← concat_comp_IccInclusionRight hfg']
apply hfgU.comp
rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : b ≤ z)⟩, rfl⟩, rfl⟩
simpa [projIccCM, projIcc, h2, hz.2] using h1
filter_upwards [hf K₁ hK₁ U hU hfU, hg K₂ hK₂ U hU hgU, hfg] with i hf hg hfg x hx
by_cases hxb : x ≤ b
· rw [concat_left hfg hxb]
refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
simp [projIccCM, projIcc, hxb, x.2.1]
· replace hxb : b ≤ x := lt_of_not_ge hxb |>.le
rw [concat_right hfg hxb]
refine hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
simp [projIccCM, projIcc, hxb, x.2.2]
