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

Goal state before:
pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ canonicalFactor R w 0 ≠ 0

pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0

Tactic:
· simp_all [canonicalFactor, ne_of_gt hR]

Goal state after:
case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_5
F : ι → 𝕜 → 𝕜
h₁ : ∀ (c : ι), MeromorphicAt (F c) x
h₂ : ∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤
hF : Function.HasFiniteMulSupport F
⊢ meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤

Tactic:
simpa [finprod_eq_prod F hF, meromorphicOrderAt_prod (fun x _ ↦ h₁ x)] using fun x _ ↦ h₂ x

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₁ x

Tactic:
meromorphicOrderAt_add_of_top_left hf₂

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₁ x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
s : ↑I
hs : s ∈ Set.Icc 0 (t (n + 1))
⊢ (p ∘ fun s ↦ if s ≤ t n then Γ s else q.invFun (γ s, (↑q (Γ (t n))).2)) s = γ s

Tactic:
Function.comp_apply

Goal state after:
case succ.refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
s : ↑I
hs : s ∈ Set.Icc 0 (t (n + 1))
⊢ p (if s ≤ t n then Γ s else q.invFun (γ s, (↑q (Γ (t n))).2)) = γ s
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: t : |2⁻¹| = 2⁻¹
z : |429895798851992810179897 / 620208537104218167705600 + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
one_div (2 : ℝ),

Goal state after:
t : |2⁻¹| = 2⁻¹
z : |429895798851992810179897 / 620208537104218167705600 + log 2⁻¹| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
eta_expand

Goal state after:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (fun z ↦ interpStrip (fun a ↦ f a) z) fun a ↦ verticalStrip 0 1 a
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (interpStrip f) z

Tactic:
eta_expand

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z ↦ interpStrip (fun a ↦ f a) z) z
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a

Tactic:
simp only [mem_preimage, mem_singleton_iff, scale, smul_eq_mul]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ (z : ℂ), z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
x : ℝ
hx : x ∈ s
⊢ x ∈ Ι a b

Tactic:
rcases hx with ⟨h1, h2⟩

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
x : ℝ
h1 : min a b < x
h2 : x < max a b
⊢ x ∈ Ι a b
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ circleAverage f c R ≤ circleAverage (fun x ↦ a) c |R|

Tactic:
circleAverage,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) ≤ circleAverage (fun x ↦ a) c |R|
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) ≤ circleAverage (fun x ↦ a) c |R|

Tactic:
circleAverage,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) ≤ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, a
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_3
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)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖(f ∘ cexp) (↑ζ.re + ↑ζ.im * I)‖ ≤ C

Tactic:
hζ,

Goal state after:
case inr.refine_3
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)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖(f ∘ cexp) (↑ζ.re + ↑(π / 2) * I)‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ circleAverage f c R ≤ a

Tactic:
rw [← circleAverage_const a c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
    mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
  exact intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf
    intervalIntegrable_const (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |circleAverage f c R| ≤ circleAverage |f| c R

Tactic:
circleAverage,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |(2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| ≤ circleAverage |f| c R
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |(2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| ≤ circleAverage |f| c R

Tactic:
circleAverage,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |(2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| ≤ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ circleAverage (fun x ↦ 0) c |R| ≤ circleAverage f c R

Tactic:
circleAverage,

Goal state after:
case pos
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, 0 ≤ circleAverage f c R
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, 0 ≤ circleAverage f c R

Tactic:
circleAverage,

Goal state after:
case pos
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, 0 ≤ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ + f₂) c R = circleAverage f₁ c R + circleAverage f₂ c R

Tactic:
circleAverage,

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

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

Tactic:
circleAverage,

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

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

Tactic:
circleAverage,

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
circleAverage,

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
circleAverage,

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - circleAverage f₂ c R

Tactic:
circleAverage,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
    ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) - (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
⊢ 0 ≤ normSq (g x)

Tactic:
exact normSq_nonneg (g x)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y | y ≠ 0})
⊢ (starRingEnd ℂ) (g x) ≠ 0

Tactic:
simpa [ne_eq, map_eq_zero] using hx.2

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 {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x : ℝ
hx : x ∈ Ici 0
⊢ ↑x ∈ closure {z | 0 < z.re}

Tactic:
rwa [closure_setOfPred_lt_re]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖

Tactic:
rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
          Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
          rpow_zero, one_mul]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w)) • f z - (q • z / (q • z - W)) • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
have h₃ : ContinuousOn f (sphere 0 R) :=
        hf.2.mono <| sphere_subset_closedBall.trans_eq (closure_ball 0 hR.ne').symm

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ Real.circleAverage (fun z ↦ (z / (z - w)) • f z - (q • z / (q • z - W)) • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R : ℝ
w c : ℂ
hw : w ∈ ball c R
⊢ ∃ d > 0, ball w d ⊆ ball c R ∧ ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖

Tactic:
have : Disjoint {w} (ball c R)ᶜ := by simpa

Goal state after:
R : ℝ
w c : ℂ
hw : w ∈ ball c R
this : Disjoint {w} (ball c R)ᶜ
⊢ ∃ d > 0, ball w d ⊆ ball c R ∧ ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : circleMap 0 R θ - x ≠ 0
⊢ HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
    ((2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)) x

Tactic:
have h₂ : HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ))
        (2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) x := by
      have h₃ := ((hasDerivAt_id' x).const_add (circleMap 0 R θ)).div
        ((hasDerivAt_id' x).const_sub (circleMap 0 R θ)) h₁
      simpa [herglotzRieszKernel_def, sub_zero, sub_sub, ← two_mul, Pi.div_def] using h₃

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : circleMap 0 R θ - x ≠ 0
h₂ : HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ)) (2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) x
⊢ HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
    ((2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)) x
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
⊢ ∀ (z : ℂ), 0 < z.re → f z = 0

Tactic:
set g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) => exp z ^ n • f z

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
⊢ ∀ (z : ℂ), 0 < z.re → f z = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite

Tactic:
use Set.univ

Goal state after:
case h
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ Set.univ ∈ nhds z ∧ (Set.univ ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
grw [norm_add_le, ← norm_sub_norm_le]
        all_goals simp only [norm_circleMap_zero, abs_of_pos hr]; grind

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

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log (‖circleMap 0 r θ‖ + R) ≤ log (2 * R) + 0 + 0

Tactic:
two_mul,

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log (‖circleMap 0 r θ‖ + R) ≤ log (R + R) + 0 + 0
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
hP : 0 < P.degree
z : ℂ
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

Tactic:
by
  have hP₀ : P ≠ 0 := by rintro rfl; simp at hP
  by_cases hPz : P.eval z = 0
  · simp [derivRootWeight, hPz, hP₀]
  · simp only [derivRootWeight, if_neg hPz]
    apply Finset.sum_pos
    · intro w hw
      apply div_pos (by simp_all)
      suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]
      rintro rfl
      simp_all
    · rw [Multiset.toFinset_nonempty]
      apply Splits.roots_ne_zero (IsAlgClosed.splits _)
      rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]

Goal state after:
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < -f x

Tactic:
← h₁

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ -f x

Tactic:
← h₁

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ sqrt 0 = 0

Tactic:
simp [sqrt]

Goal state after: