awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : Membership.mem (γ := Set ℂ) {0}ᶜ q
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) q
have rw : DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))
Tactic: rw [← qParam_right_inv hh.ne' hq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have obtain : ∀ (c : ℝ) (t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)),
  DifferentiableAt ℂ (cuspFunction h f) 0
Tactic: obtain ⟨c, t⟩ := (boundedAtFilter_cuspFunction hh h_bd).bound
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have t₁ : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)
Tactic: replace t := (eventually_differentiableAt_cuspFunction_nhds_ne_zero hh hf h_hol).and t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have t₁ : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
Tactic: simp only [norm_one, Pi.one_apply, mul_one] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have obtain : ∀ (S : Set ℂ)
  (hS1 :
    ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c)
  (hS2 : IsOpen S) (hS3 : 0 ∈ S), DifferentiableAt ℂ (cuspFunction h f) 0
Tactic: obtain ⟨S, hS1, hS2, hS3⟩ := eventually_nhds_iff.mp (eventually_nhdsWithin_iff.mp t)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
Tactic: have h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0}) :=
    fun x hx ↦ (hS1 x hx.1 hx.2).1.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
⊢ BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
have h₁ : c ∈ upperBounds (norm ∘ cuspFunction h f '' (S \ {0}))
Tactic: use c
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
⊢ c ∈ upperBounds (norm ∘ cuspFunction h f '' (S \ {0}))
have h₁ : ∀ (x : ℝ), ∀ x_1 ∈ S, x_1 ∉ {0} → (norm ∘ cuspFunction h f) x_1 = x → x ≤ c
Tactic: simp only [mem_upperBounds, Set.mem_image, Set.mem_diff, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
Tactic: have hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0})) := by
    use c
    simp only [mem_upperBounds, Set.mem_image, Set.mem_diff, forall_exists_index, and_imp]
    intro y q hq hq2 hy
    simpa only [← hy, norm_one, mul_one] using (hS1 q hq hq2).2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (limUnder (𝓝[≠] 0) (cuspFunction h f))) S
Tactic: have := differentiableOn_update_limUnder_of_bddAbove (IsOpen.mem_nhds hS2 hS3) h_diff hF_bd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (limUnder (𝓝[≠] 0) (cuspFunction h f))) S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
have this₁ : DifferentiableOn ℂ (cuspFunction h f) S
Tactic: rw [← cuspFunction_zero_eq_limUnder_nhds_ne, update_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))
have suffices : Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
Tactic: suffices Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 <| cuspFunction h f 0) by
    simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a : ℂ
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) =
    a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))
have h₁ : ∀ (y : ℂ),
  update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a y : ℂ
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
have h₁ : update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) 0 =
  (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a y : ℂ
h₁ :
  update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) 0 =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
have h₂ : ∀ (hy : y ≠ 0),
  update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) =
    update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
      update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h))
have h₁ : ∀ (y : ℂ),
  update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y
have h₁ : ∀ (hy : y ≠ 0),
  update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y
Tactic: obtain hy | rfl := ne_or_eq y 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
h₁ :
  ∀ (hy : y ≠ 0),
    update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
      (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
          update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
        y
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y
have h₂ : update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) 0 =
  (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
      update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
    0
Tactic: obtain hy | rfl := ne_or_eq y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
⊢ ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
have simp : expR (B₁ * expR (c₁ * |u z|)) ≤ expR (B₂ * expR (c₂ * |u z|))
Tactic: simp only [Real.norm_eq_abs, Real.abs_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
⊢ expR (B₁ * expR (c₁ * |u z|)) ≤ expR (B₂ * expR (c₂ * |u z|))
have a₁ : 0 ≤ expR (c₁ * |u z|)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
a₁ : 0 ≤ expR (c₁ * |u z|)
a₂ : 0 ≤ B₂
⊢ expR (B₁ * expR (c₁ * |u z|)) ≤ expR (B₂ * expR (c₂ * |u z|))
have a₃ : 0 ≤ |u z|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
have this : ∀ {c₁ c₂ B₁ B₂ : ℝ},
  c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
Tactic: have : ∀ {c₁ c₂ B₁ B₂}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z,
      ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ := fun hc hB₀ hB z ↦ by
    simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
have rcases : ∀ (cf : ℝ) (hcf : cf < a) (Bf : ℝ) (hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))),
  ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
Tactic: rcases hBf with ⟨cf, hcf, Bf, hOf⟩
Cleared hypotheses: hBf
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
have rcases : ∀ (cg : ℝ) (hcg : cg < a) (Bg : ℝ) (hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))),
  ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
Tactic: rcases hBg with ⟨cg, hcg, Bg, hOg⟩
Cleared hypotheses: hBg
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
have refine : IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
Tactic: refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
have refine_1 : cf ≤ max cf cg
Tactic: refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
refine_1 : cf ≤ max cf cg
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
have refine_2 : 0 ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
have refine_3 : Bf ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
refine_3 : Bf ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
have refine_4 : cg ≤ max cf cg
Tactic: refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
refine_3 : Bf ≤ max 0 (max Bf Bg)
refine_4 : cg ≤ max cf cg
refine_5 : 0 ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
have refine_6 : Bg ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
⊢ (cobounded ℂ ⊓ l).EventuallyLE (β := ℝ) (fun (x : ℂ) ↦ ‖expR (B₁ * ‖x‖ ^ c₁)‖) fun (z : ℂ) ↦ expR (B₂ * ‖z‖ ^ c₂)
have h : ∀ (z : ℂ) (hz : 1 ≤ ‖z‖), ‖expR (B₁ * ‖z‖ ^ c₁)‖ ≤ expR (B₂ * ‖z‖ ^ c₂)
Tactic: filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
hz : 1 ≤ ‖z‖
⊢ ‖expR (B₁ * ‖z‖ ^ c₁)‖ ≤ expR (B₂ * ‖z‖ ^ c₂)
have h : expR (B₁ * ‖z‖ ^ c₁) ≤ expR (B₂ * ‖z‖ ^ c₂)
Tactic: simp only [Real.norm_eq_abs, Real.abs_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
hz : 1 ≤ ‖z‖
⊢ expR (B₁ * ‖z‖ ^ c₁) ≤ expR (B₂ * ‖z‖ ^ c₂)
have h : 0 ≤ ‖z‖ ^ c₁
Tactic: gcongr