Theorem: osgood (Ray/Hartogs/Osgood.lean)

State before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
⊢ AnalyticOn ℂ f s
Tactic:
intro c cs
State after:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c

State before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases Metric.isOpen_iff.mp o c cs with ⟨r, rp, rs⟩
State after:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
have rs : closedBall c (r / 2) ⊆ s := le_trans (Metric.closedBall_subset_ball (by linarith)) rs
State after:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases ((isCompact_closedBall _ _).bddAbove_image (ContinuousOn.mono fc rs).norm).exists_ge 0
  with ⟨b, bp, bh⟩
State after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ y ∈ (fun x => ‖f x‖) '' closedBall c (r / 2), y ≤ b
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ y ∈ (fun x => ‖f x‖) '' closedBall c (r / 2), y ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
simp only [Set.forall_mem_image] at bh
State after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
have h : Separate f c.fst c.snd (r / 2) b s :=
  { rp := by linarith
    so := o
    rs := rs
    fc := fc
    fa0 := fa0 _ _
    fa1 := fa1 _ _
    bp := bp
    fb := fun {z0 z1} z0m z1m ↦ @bh (z0, z1)
      (spheres_subset_closedBall (Set.mk_mem_prod z0m z1m)) }
State after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
⊢ AnalyticAt ℂ f c
Tactic:
have a := (osgood_h h).analyticAt
State after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
a : AnalyticAt ℂ f (c.1, c.2)
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
a : AnalyticAt ℂ f (c.1, c.2)
⊢ AnalyticAt ℂ f c
Tactic:
simpa only [Prod.mk.eta] using a
State after:
no goals

State before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ r / 2 < r
Tactic:
linarith
State after:
no goals

State before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ 0 < r / 2
Tactic:
linarith
State after:
no goals