awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun (x : ℝ) ↦ c) (Ioo r R)
this : Tendsto f (𝓝[<] R) (𝓝 (f R))
⊢ f R = c
have apply : (fun (x : ℝ) ↦ c) =ᶠ[𝓝[<] R] f
Tactic: apply tendsto_nhds_unique this (tendsto_const_nhds.congr' _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ circleAverage (fun (x : ℂ) ↦ a) c R = a
have simp : ((2 * π)⁻¹ * (2 * π)) • a = a
Tactic: simp only [circleAverage, intervalIntegral.integral_const, ← smul_assoc, sub_zero, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ ((2 * π)⁻¹ * (2 * π)) • a = a
have ring_nf : (π * π⁻¹) • a = a
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ circleAverage f c R = a
have rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a
Tactic: rw [circleAverage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a
have left : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
have arg : ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Tactic: arg 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
have arg : fun (θ : ℝ) ↦ f (circleMap c R θ)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
θ : ℝ
| f (circleMap c R θ)
have h : a
Tactic: rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a
have h : ∀ (θ : ℝ), a
Tactic: left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst_2 : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) = a
have conv : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, a) = a
Tactic: conv =>
    left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ circleAverage f₁ c R ≤ circleAverage f₂ c R
have apply : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: apply (mul_le_mul_iff_of_pos_left (by simp [pi_pos])).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have apply : ∀ x ∈ Ioo 0 (2 * π), f₁ (circleMap c R x) ≤ f₂ (circleMap c R x)
Tactic: apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf₁ hf₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ circleAverage f c R ≤ a
have rw : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |circleAverage f c R| ≤ circleAverage |f| c R
have rw : LE.le (α := ℝ) |∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| (∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ))
Tactic: rw [circleAverage, circleAverage, smul_eq_mul, smul_eq_mul, abs_mul,
    abs_of_pos (inv_pos.2 two_pi_pos), mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
⊢ 0 ≤ circleAverage f c R
have pos : ∀ (hf : CircleIntegrable f c R), 0 ≤ circleAverage f c R
Tactic: by_cases hf : CircleIntegrable f c R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
pos : ∀ (hf : CircleIntegrable f c R), 0 ≤ circleAverage f c R
⊢ 0 ≤ circleAverage f c R
have neg : ∀ (hf : ¬CircleIntegrable f c R), 0 ≤ circleAverage f c R
Tactic: by_cases hf : CircleIntegrable f c R
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : CircleIntegrable f c R
⊢ 0 ≤ circleAverage f c R
have pos : LE.le (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, 0) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: rw [← circleAverage_const 0 c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
      mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
hf : ¬CircleIntegrable f c R
⊢ 0 ≤ circleAverage f c R
have neg : LE.le (α := ℝ) 0 0
Tactic: rw [circleAverage.integral_undef hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ Eq.{u_2 + 1} (α := F) (circleAverage ((⇑L : (a : E) → F) ∘ f) c R : F) ((L : (a : E) → F) (circleAverage f c R) : F)
have unfold : HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
  (L : (a : E) → F) (HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    (L : (a : E) → F) (HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)))
have rw : HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
  HSMul.hSMul (β := F) (2 * π)⁻¹ ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
c : ℂ
R : ℝ
inst_5 : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ HSMul.hSMul (β := F) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * π)⁻¹ ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)
have e_a : Eq.{u_2 + 1} (α := F) (∫ (θ : ℝ) in 0..2 * π, ((⇑L : (a : E) → F) ∘ f) (circleMap c R θ) : F)
  ((L : (a : E) → F) (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) : F)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ circleAverage (a • f) c R = a • circleAverage f c R
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
  a • HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    a • HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
have this : SMulCommClass 𝕜 ℝ E
Tactic: have := SMulCommClass.symm ℝ 𝕜 E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
this : SMulCommClass 𝕜 ℝ E
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
    a • HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
have rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ)) =
  (2 * π)⁻¹ • HSMul.hSMul (β := E) a (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
have rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ)) =
  (2 * π)⁻¹ •
    HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: rw [circleAverage, circleAverage, circleAverage, ← smul_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ)) =
    (2 * π)⁻¹ •
      HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have e_a : ∫ (θ : ℝ) in 0..2 * π, (f₁ + f₂) (circleMap c R θ) =
  HAdd.hAdd (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ Eq.{u_1 + 1} (α := E) (circleAverage (∑ i ∈ s, f i) c R) (∑ i ∈ s, circleAverage (f i) c R)
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (∑ i ∈ s, f i) (circleMap c R θ)) =
  ∑ i ∈ s, HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f i (circleMap c R θ))
Tactic: unfold circleAverage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ Eq.{u_1 + 1} (α := E) (circleAverage (fun (z : ℂ) ↦ ∑ i ∈ s, f i z) c R) (∑ i ∈ s, circleAverage (f i) c R)
have h₁ : ∀ (x : ℂ), Eq.{u_1 + 1} (α := E) (∑ i ∈ s, f i x) ((∑ i ∈ s, f i) x)
Tactic: convert! circleAverage_sum h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
have rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ)) =
  (2 * π)⁻¹ •
    HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: rw [circleAverage, circleAverage, circleAverage, ← smul_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ)) =
    (2 * π)⁻¹ •
      HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
have e_a : ∫ (θ : ℝ) in 0..2 * π, (f₁ - f₂) (circleMap c R θ) =
  HSub.hSub (α := E) (∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ)) (∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ))
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
⊢ c +ᵥ HSMul.hSMul (β := Set ℂ) R (range fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) = sphere c |R|
have rw : c +ᵥ sphere (HSMul.hSMul (β := ℂ) R 0) (‖R‖ * 1) = sphere c |R|
Tactic: rw [range_exp_mul_I, smul_sphere R 0 zero_le_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|
have rw : circleMap c R '' Ioc 0 (2 * π) = range (circleMap c R)
Tactic: rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
rw : circleMap c R '' Ioc 0 (2 * π) = range (circleMap c R)
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|
have rw₁ : circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (0 + 2 * π)
Tactic: rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
rw : circleMap c R '' Ioc 0 (2 * π) = range (circleMap c R)
rw₁ : circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (0 + 2 * π)
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|
have rw₂ : circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (2 * π)
Tactic: rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
⊢ AnalyticAt ℝ (circleMap c R) z
have apply : AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) z
Tactic: apply analyticAt_const.add
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R z : ℝ
hz : Membership.mem (γ := Set ℝ) univ z
⊢ AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) z
have apply : AnalyticAt ℝ (F := ℂ) (fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) z
Tactic: apply analyticAt_const.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
have simp_rw : ∀ (θ : ℝ), circleMap z R θ ≠ w
Tactic: simp_rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous (Y := ℂ) fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹
have this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
Tactic: have : ∀ θ, circleMap z R θ - w ≠ 0 := by
    simp_rw [sub_ne_zero]
    exact fun θ => circleMap_ne_mem_ball hw θ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ s ∈ map (circleMap c R) (codiscrete ℝ)
have h₂f : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) univ x → ¬EventuallyConst (circleMap c R) (𝓝 x)
Tactic: apply (analyticOnNhd_circleMap c R).preimage_mem_codiscreteWithin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
h₂f : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) univ x → ¬EventuallyConst (circleMap c R) (𝓝 x)
⊢ s ∈ map (circleMap c R) (codiscrete ℝ)
have hs₁ : s ∈ codiscreteWithin (circleMap c R '' univ)
Tactic: apply (analyticOnNhd_circleMap c R).preimage_mem_codiscreteWithin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
hCon : EventuallyConst (circleMap c R) (𝓝 x)
⊢ False
have h₂f : ∀ (a : ℂ) (ha : circleMap c R =ᶠ[𝓝 x] fun (x : ℝ) ↦ a), False
Tactic: obtain ⟨a, ha⟩ := eventuallyConst_iff_exists_eventuallyEq.1 hCon
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (hypothesis)
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x
hCon : EventuallyConst (circleMap c R) (𝓝 x)
a : ℂ
ha : circleMap c R =ᶠ[𝓝 x] fun (x : ℝ) ↦ a
⊢ False
have this : deriv (circleMap c R) x = deriv (fun (x : ℝ) ↦ a) x
Tactic: have := ha.deriv.eq_of_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ s ∈ codiscreteWithin (circleMap c R '' univ)
have hs₁ : s ∈ codiscreteWithin (range (circleMap c R))
Tactic: rwa [Set.image_univ, range_circleMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ i ∈ s, f i) c R
have rw : IntervalIntegrable.{u_1} (ε := E) (∑ i ∈ s, fun (θ : ℝ) ↦ f i (circleMap c R θ)) volume 0 (2 * π)
Tactic: rw [CircleIntegrable, (by aesop : (fun θ ↦ (∑ i ∈ s, f i) (circleMap c R θ))
    = ∑ i ∈ s, fun θ ↦ f i (circleMap c R θ))] at *
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ ∑ i ∈ s, f i z) c R
have h₁ : ∀ (x : ℂ), Eq.{u_1 + 1} (α := E) (∑ i ∈ s, f i x) ((∑ i ∈ s, f i) x)
Tactic: convert! CircleIntegrable.sum s h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
have pos : ∀ (h₁ : (support f).Finite), CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
Tactic: by_cases h₁ : (Function.support f).Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
pos : ∀ (h₁ : (support f).Finite), CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
have neg : ∀ (h₁ : ¬(support f).Finite), CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
Tactic: by_cases h₁ : (Function.support f).Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : (support f).Finite
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
have pos : CircleIntegrable.{u_1} (E := E) (∑ i ∈ h₁.toFinset (s := support f), f i) c R
Tactic: rw [finsum_eq_sum f h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : ¬(support f).Finite
⊢ CircleIntegrable.{u_1} (E := E) (∑ᶠ (i : ι), f i) c R
have neg : CircleIntegrable.{u_1} (E := E) 0 c R
Tactic: rw [finsum_of_infinite_support h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst_1 : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (θ : ℝ) ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
have simp : ∀
  (hf :
    IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π))
      volume),
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
Tactic: simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst_1 : NormedSpace ℂ E
hf :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
have refine_1 : AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
  (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
Tactic: refine (hf.norm.const_mul |R|).mono' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst_1 : NormedSpace ℂ E
hf :
  IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace) (fun (θ : ℝ) ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
refine_1 :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (fun (θ : ℝ) ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
have refine_2 : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
  ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖
Tactic: refine (hf.norm.const_mul |R|).mono' ?_ ?_