Theory Winding_Number_Eval.Missing_Analysis

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Some useful lemmas in analysis›

theory Missing_Analysis
  imports "HOL-Analysis.Analysis"
begin  

subsection ‹More about paths›
   
lemma pathfinish_offset[simp]:
  "pathfinish (λt. g t - z) = pathfinish g - z"
  unfolding pathfinish_def by simp 
    
lemma pathstart_offset[simp]:
  "pathstart (λt. g t - z) = pathstart g - z"
  unfolding pathstart_def by simp
    
lemma pathimage_offset[simp]:
  fixes g :: "_ ⇒ 'b::topological_group_add"
  shows "p ∈ path_image (λt. g t - z) ⟷ p+z ∈ path_image g " 
unfolding path_image_def by (auto simp:algebra_simps)
  
lemma path_offset[simp]:
 fixes g :: "_ ⇒ 'b::topological_group_add"
 shows "path (λt. g t - z) ⟷ path g"
unfolding path_def
proof 
  assume "continuous_on {0..1} (λt. g t - z)" 
  hence "continuous_on {0..1} (λt. (g t - z) + z)"
    using continuous_on_add continuous_on_const by blast 
  then show "continuous_on {0..1} g" by auto
qed (auto intro:continuous_intros)   
   
end