mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ cexp) =O[comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2)) ⊔ comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦
    expR (max B 0 * expR (c * |z.re|))

Tactic:
]

Goal state after:
case inr.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ cexp) =O[comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2)) ⊔ comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦
    expR (max B 0 * expR (c * |z.re|))
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ (2 * ↑π * I)⁻¹ • (2 * ↑π * I) • f w = f w

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ (2 * ↑π * I)⁻¹ • (2 * ↑π * I) • f w = f w
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
⊢ ContinuousOn f (closedBall c |R|)

Tactic:
simpa [← closure_ball _ (ne_of_not_ge hR).symm] using hf.2

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) = fderiv ℝ f y

Tactic:
]

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) = fderiv ℝ f y
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
z : ℂ
hz : z ∈ ball c |R|
⊢ DifferentiableAt ℂ f z

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
z : ℂ
hz : z ∈ ball c |R|
⊢ DifferentiableAt ℂ f z
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc✝ : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
w : ℂ
⊢ 0 ≤ max B 0 * expR (c * |w.re|)

Tactic:
]

Goal state after:
case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc✝ : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
w : ℂ
⊢ 0 ≤ max B 0 * expR (c * |w.re|)
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) a = (fderiv ℝ f y) (a.re • 1 + a.im • I)

Tactic:
]

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) a = (fderiv ℝ f y) (a.re • 1 + a.im • I)
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
⊢ circleAverage f c R = circleAverage (fun z ↦ ((z - c) / (z - c)) • f z) c R

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
⊢ circleAverage f c R = circleAverage (fun z ↦ ((z - c) / (z - c)) • f z) c R
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = Real.circleAverage (fun z ↦ ((z - c) / (z - c)) • f z) c R

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = Real.circleAverage (fun z ↦ ((z - c) / (z - c)) • f z) c R
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) a = a.re • (fderiv ℝ f y) 1 + a.im • (fderiv ℝ f y) I

Tactic:
]

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) a = a.re • (fderiv ℝ f y) 1 + a.im • (fderiv ℝ f y) I
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ) = f c

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst✝ : CompleteSpace E
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ) = f c
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (↑(2 * π))⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (I⁻¹ * (2 * ↑π)⁻¹ * I) • ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)

Tactic:
]

Goal state after:
c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (↑(2 * π))⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (I⁻¹ * (2 * ↑π)⁻¹ * I) • ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
]

Goal state after:
case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f {x}
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
⊢ circleAverage f c R = circleAverage f c R

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
a✝ : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B * expR (c * x) ≤ max B 0 * expR (c * x)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
a✝ : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B * expR (c * x) ≤ max B 0 * expR (c * x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : R < 0
⊢ circleAverage f c R = circleAverage f c R

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ (⇑reCLM ∘ F) x = f x

Tactic:
]

Goal state after:
case right
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ (⇑reCLM ∘ F) x = f x
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
]

Goal state after:
case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x) = ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (x : ℝ) in -(2 * π)..-0, f (circleMap 0 1 x) = ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
⊢ ∀ (g : StrongDual ℝ F), g (circleAverage f c R) = g (f c)

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
⊢ ∀ (g : StrongDual ℝ F), g (circleAverage f c R) = g (f c)
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
⊢ circleAverage (⇑g ∘ f) c R = g (f c)

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
⊢ circleAverage (⇑g ∘ f) c R = g (f c)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z | ‖z - c‖ ∈ s}.domRestrict f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s.domRestrict (Real.circleAverage f c))

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z | ‖z - c‖ ∈ s}.domRestrict f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s.domRestrict (Real.circleAverage f c))
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
⊢ circleAverage (⇑g ∘ f) c R = g (f c)

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
⊢ circleAverage (⇑g ∘ f) c R = g (f c)
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : y ∈ univ
⊢ fderiv ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y = fderiv ℝ f y

Tactic:
]

Goal state after:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : y ∈ univ
⊢ fderiv ℝ (⇑reCLM) (F y) ∘SL fderiv ℝ F y = fderiv ℝ f y
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R

Tactic:
]

Goal state after:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖f ↑(expR ζ)‖ ≤ C

Tactic:
]

Goal state after:
case inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖f ↑(expR ζ)‖ ≤ C
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball x ε)
h₂F : EqOn (fun z ↦ (F z).re) f (ball x ε)
⊢ AnalyticAt ℝ (fun y ↦ (F y).re) x

Tactic:
]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball x ε)
h₂F : EqOn (fun z ↦ (F z).re) f (ball x ε)
⊢ AnalyticAt ℝ (fun y ↦ (F y).re) x