[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
set r : ℝ := dist w z
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
have hw : w ∈ closedBall z r := mem_closedBall.2 le_rfl
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
refine' (isMaxOn_iff.1 hz _ hw).antisymm (not_lt.1 _)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
⊢ ¬(norm ∘ f) w < (norm ∘ f) z
[PROOFSTEP]
rintro hw_lt : ‖f w‖ < ‖f z‖
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
⊢ False
[PROOFSTEP]
have hr : 0 < r :=
  dist_pos.2
    (ne_of_apply_ne (norm ∘ f) hw_lt.ne)
      -- Due to Cauchy integral formula, it suffices to prove the following inequality.
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ False
[PROOFSTEP]
suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
  by
  refine' this.ne _
  have A : (∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * π * I : ℂ) • f z :=
    hd.circleIntegral_sub_inv_smul (mem_ball_self hr)
  simp [A, norm_smul, Real.pi_pos.le]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
⊢ False
[PROOFSTEP]
refine' this.ne _
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ = 2 * π * ‖f z‖
[PROOFSTEP]
have A : (∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * π * I : ℂ) • f z := hd.circleIntegral_sub_inv_smul (mem_ball_self hr)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
A : (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * ↑π * I) • f z
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ = 2 * π * ‖f z‖
[PROOFSTEP]
simp [A, norm_smul, Real.pi_pos.le]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
[PROOFSTEP]
suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r) by
  rwa [mul_assoc, mul_div_cancel' _ hr.ne'] at this
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
[PROOFSTEP]
rwa [mul_assoc, mul_div_cancel' _ hr.ne'] at this
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
[PROOFSTEP]
have hsub : sphere z r ⊆ closedBall z r := sphere_subset_closedBall
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
[PROOFSTEP]
refine' circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr _ _ ⟨w, rfl, _⟩
[GOAL]
case refine'_1
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ContinuousOn (fun ζ => (ζ - z)⁻¹ • f ζ) (sphere z r)
case refine'_2
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ∀ (z_1 : ℂ), z_1 ∈ sphere z r → ‖(z_1 - z)⁻¹ • f z_1‖ ≤ ‖f z‖ / r
case refine'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
[PROOFSTEP]
show ContinuousOn (fun ζ : ℂ => (ζ - z)⁻¹ • f ζ) (sphere z r)
[GOAL]
case refine'_1
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ContinuousOn (fun ζ => (ζ - z)⁻¹ • f ζ) (sphere z r)
[PROOFSTEP]
refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub)
[GOAL]
case refine'_1
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ∀ (x : ℂ), x ∈ sphere z r → _root_.id x - z ≠ 0
[PROOFSTEP]
exact fun ζ hζ => sub_ne_zero.2 (ne_of_mem_sphere hζ hr.ne')
[GOAL]
case refine'_2
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ∀ (z_1 : ℂ), z_1 ∈ sphere z r → ‖(z_1 - z)⁻¹ • f z_1‖ ≤ ‖f z‖ / r
case refine'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
[PROOFSTEP]
show ∀ ζ ∈ sphere z r, ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r
[GOAL]
case refine'_2
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ∀ (ζ : ℂ), ζ ∈ sphere z r → ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r
[PROOFSTEP]
rintro ζ (hζ : abs (ζ - z) = r)
[GOAL]
case refine'_2
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ↑abs (ζ - z) = r
⊢ ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r
[PROOFSTEP]
rw [le_div_iff hr, norm_smul, norm_inv, norm_eq_abs, hζ, mul_comm, mul_inv_cancel_left₀ hr.ne']
[GOAL]
case refine'_2
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ↑abs (ζ - z) = r
⊢ ‖f ζ‖ ≤ ‖f z‖
[PROOFSTEP]
exact hz (hsub hζ)
[GOAL]
case refine'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
[PROOFSTEP]
show ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
[GOAL]
case refine'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
[PROOFSTEP]
rw [norm_smul, norm_inv, norm_eq_abs, ← div_eq_inv_mul]
[GOAL]
case refine'_3
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖f w‖ / ↑abs (w - z) < ‖f z‖ / r
[PROOFSTEP]
exact (div_lt_div_right hr).2 hw_lt
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖↑e x‖ = ‖x‖
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z
[GOAL]
case hz
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖↑e x‖ = ‖x‖
⊢ IsMaxOn (norm ∘ ↑e ∘ f) (closedBall z (dist w z)) z
[PROOFSTEP]
simpa only [IsMaxOn, (· ∘ ·), he] using hz
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖↑e x‖ = ‖x‖
hz : IsMaxOn (norm ∘ ↑e ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
simpa only [he, (· ∘ ·)] using norm_max_aux₁ (e.differentiable.comp_diffContOnCl hd) hz
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
subst r
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
rcases eq_or_ne w z with (rfl | hne)
[GOAL]
case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖
[PROOFSTEP]
rfl
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
rw [← dist_ne_zero] at hne
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne✝ : w ≠ z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖
[PROOFSTEP]
exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ EqOn (norm ∘ f) (Function.const E ‖f z‖) (closedBall z r)
[PROOFSTEP]
intro w hw
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
rw [mem_closedBall, dist_comm] at hw
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
rcases eq_or_ne z w with (rfl | hne)
[GOAL]
case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z
[PROOFSTEP]
rfl
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
set e := (lineMap z w : ℂ → E)
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
this : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
[PROOFSTEP]
simpa
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
[PROOFSTEP]
have hr : dist (1 : ℂ) 0 = 1 := by simp
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ dist 1 0 = 1
[PROOFSTEP]
simp
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
[PROOFSTEP]
have hball : MapsTo e (ball 0 1) (ball z r) :=
  by
  refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono Subset.rfl ?_
  simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ MapsTo e (ball 0 1) (ball z r)
[PROOFSTEP]
refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono Subset.rfl ?_
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ball (↑(lineMap z w) 0) (↑(nndist z w) * 1) ⊆ ball z r
[PROOFSTEP]
simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw
[GOAL]
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
hball : MapsTo e (ball 0 1) (ball z r)
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
[PROOFSTEP]
exact norm_max_aux₃ hr (hd.comp hde.diffContOnCl hball) (hz.comp_mapsTo hball (lineMap_apply_zero z w))
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
[GOAL]
case intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (fun x => (norm ∘ f) x ≤ (norm ∘ f) c) x
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
exact
  nhds_basis_closedBall.eventually_iff.2
    ⟨r, hr₀,
      norm_eqOn_closedBall_of_isMaxOn
        (DifferentiableOn.diffContOnCl fun x hx => (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt)
        fun x hx => (hr <| ball_subset_closedBall hx).2⟩
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
⊢ IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
[PROOFSTEP]
refine' isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and _
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
⊢ ∀ᶠ (z : E) in 𝓝 z, IsMaxOn (norm ∘ f) s z
[PROOFSTEP]
replace hd : ∀ᶠ w in 𝓝 z, DifferentiableAt ℂ f w
[GOAL]
case hd
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
⊢ ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ ∀ᶠ (z : E) in 𝓝 z, IsMaxOn (norm ∘ f) s z
[PROOFSTEP]
exact hd.eventually_differentiableAt hz.1
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ ∀ᶠ (z : E) in 𝓝 z, IsMaxOn (norm ∘ f) s z
[PROOFSTEP]
exact (norm_eventually_eq_of_isLocalMax hd <| hz.2.isLocalMax hz.1).mono fun x hx y hy => le_trans (hz.2 hy).out hx.ge
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
[PROOFSTEP]
set V := U ∩ {z | IsMaxOn (norm ∘ f) U z}
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
[PROOFSTEP]
have hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖ := fun x hx => le_antisymm (hm hx.1) (hx.2 hcU)
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
[PROOFSTEP]
suffices : U ⊆ V
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
this : U ⊆ V
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
⊢ U ⊆ V
[PROOFSTEP]
exact fun x hx => hV x (this hx)
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
⊢ U ⊆ V
[PROOFSTEP]
have hVo : IsOpen V := by
  simpa only [ho.mem_nhds_iff, setOf_and, setOf_mem_eq] using isOpen_setOf_mem_nhds_and_isMaxOn_norm hd
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
⊢ IsOpen V
[PROOFSTEP]
simpa only [ho.mem_nhds_iff, setOf_and, setOf_mem_eq] using isOpen_setOf_mem_nhds_and_isMaxOn_norm hd
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
⊢ U ⊆ V
[PROOFSTEP]
have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, hm⟩
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
⊢ U ⊆ V
[PROOFSTEP]
set W := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
⊢ U ⊆ V
[PROOFSTEP]
have hWo : IsOpen W := hd.continuousOn.norm.preimage_open_of_open ho isOpen_ne
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen W
⊢ U ⊆ V
[PROOFSTEP]
have hdVW : Disjoint V W := disjoint_left.mpr fun x hxV hxW => hxW.2 (hV x hxV)
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen W
hdVW : Disjoint V W
⊢ U ⊆ V
[PROOFSTEP]
have hUVW : U ⊆ V ∪ W := fun x hx =>
  (eq_or_ne ‖f x‖ ‖f c‖).imp (fun h => ⟨hx, fun y hy => (hm hy).out.trans_eq h.symm⟩) (And.intro hx)
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ (x : E), x ∈ V → ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen W
hdVW : Disjoint V W
hUVW : U ⊆ V ∪ W
⊢ U ⊆ V
[PROOFSTEP]
exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : E
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖
[PROOFSTEP]
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
s : Set E
z w : E
hd : DiffContOnCl ℂ f s
hz : IsMaxOn (norm ∘ f) s z
hsub : ball z (dist w z) ⊆ s
H₁ : ‖f w‖ = ‖f z‖
H₂ : ‖f w + f z‖ = ‖f z + f z‖
⊢ ‖f w + f z‖ = ‖f w‖ + ‖f z‖
[PROOFSTEP]
simp only [H₂, SameRay.rfl.norm_add, H₁]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c
[PROOFSTEP]
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
[GOAL]
case intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (fun x => (norm ∘ f) x ≤ (norm ∘ f) c) x
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c
[PROOFSTEP]
exact
  nhds_basis_closedBall.eventually_iff.2
    ⟨r, hr₀,
      eqOn_closedBall_of_isMaxOn_norm
        (DifferentiableOn.diffContOnCl fun x hx => (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt)
        fun x hx => (hr <| ball_subset_closedBall hx).2⟩
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
⊢ (∀ᶠ (z : E) in 𝓝 c, f z = f c) ∨ f c = 0
[PROOFSTEP]
refine' or_iff_not_imp_right.mpr fun h => _
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
[PROOFSTEP]
have h1 : ∀ᶠ z in 𝓝 c, f z ≠ 0 := hf.self_of_nhds.continuousAt.eventually_ne h
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
[PROOFSTEP]
have h2 : IsLocalMax (norm ∘ f)⁻¹ c := hc.inv (h1.mono fun z => norm_pos_iff.mpr)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
[PROOFSTEP]
have h3 : IsLocalMax (norm ∘ f⁻¹) c := by refine' h2.congr (eventually_of_forall _); simp
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ IsLocalMax (norm ∘ f⁻¹) c
[PROOFSTEP]
refine' h2.congr (eventually_of_forall _)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x
[PROOFSTEP]
simp
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
[PROOFSTEP]
have h4 : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f⁻¹ z := by filter_upwards [hf, h1] with z h using h.inv
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z
[PROOFSTEP]
filter_upwards [hf, h1] with z h using h.inv
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
h4 : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
[PROOFSTEP]
filter_upwards [eventually_eq_of_isLocalMax_norm h4 h3] with z using inv_inj.mp
[GOAL]
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
have hc : IsCompact (closure U) := hb.isCompact_closure
[GOAL]
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w
[GOAL]
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
⊢ ∃ w, w ∈ closure U ∧ IsMaxOn (norm ∘ f) (closure U) w
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
exact hc.exists_forall_ge hne.closure hd.continuousOn.norm
[GOAL]
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ closure U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
rw [closure_eq_interior_union_frontier, mem_union] at hwU
[GOAL]
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure U) w
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
cases' hwU with hwU hwU
[GOAL]
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro.inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ frontier U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
exact ⟨w, hwU, hle⟩
[GOAL]
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure
[GOAL]
case intro.intro.inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩
[GOAL]
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
⊢ ∃ z, z ∈ frontier U ∧ IsMaxOn (norm ∘ f) (closure U) z
[PROOFSTEP]
refine' ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq _⟩
[GOAL]
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure U
⊢ (norm ∘ f) w = (norm ∘ f) z
[PROOFSTEP]
refine' (norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) _).symm
[GOAL]
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (dist z w) ⊆ U
[PROOFSTEP]
rw [dist_comm, ← hzw]
[GOAL]
case intro.intro.inl.intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Metric.Bounded U
hne : Set.Nonempty U
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure U)
w : E
hle : IsMaxOn (norm ∘ f) (closure U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure U
⊢ ball w (infDist w (interior U)ᶜ) ⊆ U
[PROOFSTEP]
exact ball_infDist_compl_subset.trans interior_subset
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ closure U
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
cases' hz with hz hz
[GOAL]
case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
exact hC z hz
[GOAL]
case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
rcases exists_ne z with ⟨w, hne⟩
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
set e := (lineMap z w : ℂ → E)
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
[GOAL]
case hd
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
exact hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [mem_preimage, lineMap_apply_zero]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ 0 ∈ e ⁻¹' U
[PROOFSTEP]
simpa only [mem_preimage, lineMap_apply_zero]
[GOAL]
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
rcases exists_mem_frontier_isMaxOn_norm (hL.bounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
[GOAL]
case inr.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C
[PROOFSTEP]
calc
  ‖f z‖ = ‖f (e 0)‖ := by simp only [lineMap_apply_zero]
  _ ≤ ‖f (e ζ)‖ := (hζ (subset_closure h₀))
  _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ = ‖f (e 0)‖
[PROOFSTEP]
simp only [lineMap_apply_zero]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Metric.Bounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ EqOn f g (closure U)
[PROOFSTEP]
suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Metric.Bounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
H : ∀ (z : E), z ∈ closure U → ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure U)
[PROOFSTEP]
simpa [sub_eq_zero] using H
[GOAL]
case H
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Metric.Bounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ ∀ (z : E), z ∈ closure U → ‖(f - g) z‖ ≤ 0
[PROOFSTEP]
refine' fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => _) hz
[GOAL]
case H
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Metric.Bounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
z : E
hz : z ∈ closure U
w : E
hw : w ∈ frontier U
⊢ ‖(f - g) w‖ ≤ 0
[PROOFSTEP]
simp [hfg hw]


[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) y) = inner (↑T y) x
[PROOFSTEP]
rw [hT x y, inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
⊢ IsSymmetric (T + S)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner (↑(T + S) x) y = inner x (↑(T + S) y)
[PROOFSTEP]
rw [LinearMap.add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner x (↑T y + ↑S y) = inner x (↑(T + S) y)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ Continuous ↑T
[PROOFSTEP]
refine' T.continuous_of_seq_closed_graph fun u x y hu hTu => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ y = ↑T x
[PROOFSTEP]
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ inner (y - ↑T x) (y - ↑T x) = 0
[PROOFSTEP]
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ :=
  by
  intro k
  rw [← T.map_sub, hT]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
[PROOFSTEP]
intro k
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
k : ℕ
⊢ inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
[PROOFSTEP]
rw [← T.map_sub, hT]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ inner (y - ↑T x) (y - ↑T x) = 0
[PROOFSTEP]
refine' tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner ((↑T ∘ u) t - ↑T x) (y - ↑T x)) Filter.atTop (nhds 0)
[PROOFSTEP]
simp_rw [Function.comp_apply, hlhs]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds 0)
[PROOFSTEP]
rw [← inner_zero_left (T (y - T x))]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds (inner 0 (↑T (y - ↑T x))))
[PROOFSTEP]
refine' Filter.Tendsto.inner _ tendsto_const_nhds
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)
[PROOFSTEP]
rw [← sub_self x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℝ E'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
[PROOFSTEP]
exact hu.sub_const _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
[PROOFSTEP]
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
r : ℝ
hr : inner (↑T x) x = ↑r
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
[PROOFSTEP]
simp [hr, T.reApplyInnerSelf_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ∃ r, inner (↑T x) x = ↑r
[PROOFSTEP]
rw [← conj_eq_iff_real]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) x) = inner (↑T x) x
[PROOFSTEP]
exact hT.conj_inner_sym x x
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ inner (↑(↑ℝ T) x) y = inner x (↑(↑ℝ T) y)
[PROOFSTEP]
simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T ↔ ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T → ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
intro hT v
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : IsSymmetric T
v : V
⊢ ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
apply IsSymmetric.conj_inner_sym hT
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v) → IsSymmetric T
[PROOFSTEP]
intro h x y
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = inner x (↑T y)
[PROOFSTEP]
rw [← inner_conj_symm x (T y)]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = ↑(starRingEnd ℂ) (inner (↑T y) x)
[PROOFSTEP]
rw [inner_map_polarization T x y]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    ↑(starRingEnd ℂ)
      ((inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
            Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) -
          Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
        4)
[PROOFSTEP]
simp only [starRingEnd_apply, star_div', star_sub, star_add, star_mul]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (star (inner (↑T (x + y)) (x + y)) - star (inner (↑T (x - y)) (x - y)) +
          star (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * star Complex.I -
        star (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * star Complex.I) /
      star 4
[PROOFSTEP]
simp only [← starRingEnd_apply]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (↑(starRingEnd ℂ) (inner (↑T (x + y)) (x + y)) - ↑(starRingEnd ℂ) (inner (↑T (x - y)) (x - y)) +
          ↑(starRingEnd ℂ) (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I -
        ↑(starRingEnd ℂ) (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
[PROOFSTEP]
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * ↑(starRingEnd ℂ) Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
[PROOFSTEP]
simp only [Complex.conj_I]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
[PROOFSTEP]
rw [inner_map_polarization']
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) -
          Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) +
        Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
      4 =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
[PROOFSTEP]
norm_num
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) -
          Complex.I * inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) +
        Complex.I * inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y)) /
      4 =
    (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) +
          -(inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) * Complex.I) +
        inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y) * Complex.I) /
      4
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
[PROOFSTEP]
rcases@I_mul_I_ax 𝕜 _ with (h | h)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
[PROOFSTEP]
simp_rw [h, zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left,
  inner_sub_right, hT x, ← inner_conj_symm x (T y)]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(starRingEnd 𝕜) (inner (↑T y) x) =
    (inner x (↑T x) + ↑(starRingEnd 𝕜) (inner (↑T y) x) + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - ↑(starRingEnd 𝕜) (inner (↑T y) x) - (inner (↑T y) x - inner (↑T y) y))) /
      4
[PROOFSTEP]
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
  rw [conj_eq_iff_re.mpr this]
  ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
this : ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
⊢ ↑(starRingEnd 𝕜) (inner (↑T y) x) =
    (inner x (↑T x) + ↑(starRingEnd 𝕜) (inner (↑T y) x) + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - ↑(starRingEnd 𝕜) (inner (↑T y) x) - (inner (↑T y) x - inner (↑T y) y))) /
      4
[PROOFSTEP]
rw [conj_eq_iff_re.mpr this]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
this : ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
⊢ inner (↑T y) x =
    (inner x (↑T x) + inner (↑T y) x + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - inner (↑T y) x - (inner (↑T y) x - inner (↑T y) y))) /
      4
[PROOFSTEP]
ring
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
[PROOFSTEP]
rw [← re_add_im ⟪T y, x⟫]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I)) = ↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I
[PROOFSTEP]
simp_rw [h, mul_zero, add_zero]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re ↑(↑re (inner (↑T y) x))) = ↑(↑re (inner (↑T y) x))
[PROOFSTEP]
norm_cast
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
[PROOFSTEP]
simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, LinearMap.map_smul,
  inner_smul_left, inner_smul_right, IsROrC.conj_I, mul_add, mul_sub, sub_sub, ← mul_assoc, mul_neg, h, neg_neg,
  one_mul, neg_one_mul]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T x) x + inner (↑T x) y + (inner (↑T y) x + inner (↑T y) y) -
          (inner (↑T x) x - (inner (↑T x) y + (inner (↑T y) x - inner (↑T y) y)) +
            (I * inner (↑T x) x + -inner (↑T x) y + (inner (↑T y) x + I * inner (↑T y) y))) +
        (I * inner (↑T x) x - (-inner (↑T x) y + (inner (↑T y) x - I * inner (↑T y) y)))) /
      4
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ (∀ (x : E), inner (↑T x) x = 0) ↔ T = 0
[PROOFSTEP]
simp_rw [LinearMap.ext_iff, zero_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ (∀ (x : E), inner (↑T x) x = 0) ↔ ∀ (x : E), ↑T x = 0
[PROOFSTEP]
refine' ⟨fun h x => _, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), ↑T x = 0
⊢ ∀ (x : E), inner (↑T x) x = 0
[PROOFSTEP]
simp_rw [h, inner_zero_left, forall_const]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ ↑T x = 0
[PROOFSTEP]
rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ (inner (↑T (x + ↑T x)) (x + ↑T x) - inner (↑T (x - ↑T x)) (x - ↑T x) - I * inner (↑T (x + I • ↑T x)) (x + I • ↑T x) +
        I * inner (↑T (x - I • ↑T x)) (x - I • ↑T x)) /
      4 =
    0
[PROOFSTEP]
simp_rw [h _]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ (0 - 0 - I * 0 + I * 0) / 4 = 0
[PROOFSTEP]
ring


[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
rcases coercive with ⟨C, C_ge_0, coercivity⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
refine' ⟨C, C_ge_0, _⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
intro v
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
by_cases h : 0 < ‖v‖
[GOAL]
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
refine' (mul_le_mul_right h).mp _
[GOAL]
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖ * ‖v‖
[PROOFSTEP]
calc
  C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
  _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
  _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v
[GOAL]
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
have : v = 0 := by simpa using h
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
⊢ v = 0
[PROOFSTEP]
simpa using h
[GOAL]
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
v : V
h : ¬0 < ‖v‖
this : v = 0
⊢ C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
[PROOFSTEP]
simp [this]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
refine' ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), _⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ AntilipschitzWith (Real.toNNReal C⁻¹) ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
refine' ContinuousLinearMap.antilipschitz_of_bound B♯ _
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ ↑(Real.toNNReal C⁻¹) * ‖↑(continuousLinearMapOfBilin B) x‖
[PROOFSTEP]
simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ← inv_mul_le_iff (inv_pos.mpr C_pos)]
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖↑(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ ‖↑(continuousLinearMapOfBilin B) x‖
[PROOFSTEP]
simpa using below_bound
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ker (continuousLinearMapOfBilin B) = ⊥
[PROOFSTEP]
rw [LinearMapClass.ker_eq_bot]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
[PROOFSTEP]
exact antilipschitz.injective
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
[PROOFSTEP]
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
[PROOFSTEP]
exact antilipschitz.isClosed_range B♯.uniformContinuous
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ range (continuousLinearMapOfBilin B) = ⊤
[PROOFSTEP]
haveI := coercive.closed_range.completeSpace_coe
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ range (continuousLinearMapOfBilin B) = ⊤
[PROOFSTEP]
rw [← (range B♯).orthogonal_orthogonal]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ (range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤
[PROOFSTEP]
rw [Submodule.eq_top_iff']
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ ∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ
[PROOFSTEP]
intro v w mem_w_orthogonal
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ inner w v = 0
[PROOFSTEP]
rcases coercive with ⟨C, C_pos, coercivity⟩
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ inner w v = 0
[PROOFSTEP]
obtain rfl : w = 0 :=
  by
  rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ← mul_assoc]
  apply le_antisymm
  ·
    calc
      C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
      _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
      _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
  · exact mul_nonneg (mul_nonneg C_pos.le (norm_nonneg w)) (norm_nonneg w)
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ w = 0
[PROOFSTEP]
rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ← mul_assoc]
[GOAL]
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ = 0
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0
[PROOFSTEP]
calc
  C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
  _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
  _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
[GOAL]
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖
[PROOFSTEP]
exact mul_nonneg (mul_nonneg C_pos.le (norm_nonneg w)) (norm_nonneg w)
[GOAL]
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v : V
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ↑(↑B u) u
mem_w_orthogonal : 0 ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ inner 0 v = 0
[PROOFSTEP]
exact inner_zero_left _