E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
cases' eq_or_ne (dslope f c z) 0 with hc hc
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have hg' : ‖g‖₊ = 1 := NNReal.eq hg
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
no goals
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
calc
  ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ := by
    rw [g.dslope_comp, hgf, IsROrC.norm_ofReal, abs_norm]
    exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
  _ ≤ R₂ / R₁ := by
    refine' schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp _ h_maps) hz
    simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ 0 ≤ R₂ / R₁
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
rw [hc, norm_zero]
no goals
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ 0 ≤ R₂ / R₁
exact div_nonneg hR₂.le hR₁.le
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖g‖₊ ≠ 0
simpa only [hg'] using one_ne_zero
case H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ c = z → DifferentiableAt ℂ f c
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ = ‖dslope (↑g ∘ f) c z‖
rw [g.dslope_comp, hgf, IsROrC.norm_ofReal, abs_norm]
no goals
case H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ c = z → DifferentiableAt ℂ f c
exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ MapsTo (↑g) (ball (f c) R₂) (ball ((↑g ∘ f) c) R₂)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope (↑g ∘ f) c z‖ ≤ R₂ / R₁
refine' schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp _ h_maps) hz
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ MapsTo (↑g) (ball (f c) R₂) (ball ((↑g ∘ f) c) R₂)
simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂