awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
z₁ : ℂ
hz₁ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₁
z₂ : ℂ
hz₂ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₂
hR₁ : ¬R = 0
hz₃ : ‖z‖ = 1
hz₄ : ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0
⊢ ‖z₂‖ = 1 ∧ z₂ + (↑R : ℂ)⁻¹ * (c - a) = 0

Tactic:
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]

Premises used: sub_zero, Set.mem_setOf_eq, ne_eq, mem_sphere_iff_norm, Set.mem_diff, Decidable.not_not, abs_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
z z₁ z₂ : ℂ
hR : ¬R = 0
hz : ‖z‖ = 1
hz₁ : ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0
hz₂ : ‖z₂‖ = 1 ∧ z₂ + (↑R : ℂ)⁻¹ * (c - a) = 0
h : -((↑R : ℂ)⁻¹ * (c - a)) = z₂
h₁ h₂ : -((↑R : ℂ)⁻¹ * (c - a)) = -((↑R : ℂ)⁻¹ * (c - a))
⊢ z₁ = z₂

Tactic:
rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]

Premises used: add_eq_zero_iff_eq_neg, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}

Tactic:
have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
h :
  ∀ (z : ℂ) (hz : ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0),
    log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖)
    fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖

Tactic:
filter_upwards [this] with z hz
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
z : ℂ
hz : ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0
h : log ‖(↑R : ℂ)‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
⊢ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖

Tactic:
rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, norm_mul, norm_ne_zero_iff, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
z : ℂ
hz : ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0
⊢ log ‖(↑R : ℂ)‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
x : ℂ
h : Membership.mem (γ := Set ℂ) (sphere 0 |1|) x
⊢ MeromorphicAt (E := ℂ) (fun (z : ℂ) ↦ z + (↑R⁻¹ : ℂ) * (c - a)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
rw : log ‖R‖ + circleAverage (fun (x : ℂ) ↦ log ‖x + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
⊢ circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)

Tactic:
rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]

Premises used: Norm.norm, Real.log, Pi.add_def, Real.circleAverage_add, OfNat.ofNat, MeromorphicOn.circleIntegrable_log_norm, circleIntegrable_const, Real.circleAverage_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ log ‖R‖ + circleAverage (fun (x : ℂ) ↦ log ‖x + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
e_a : log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
⊢ log R + log⁺ (|R|⁻¹ * ‖c - a‖) = log R + log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
e_a : ∀ (h : R < 0), log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
e_a₁ : ∀ (h : 0 < R), log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
rcases hR.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
h : R < 0
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
simp [abs_of_neg h]

Premises used: abs_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
e_a e_a₁ : log⁺ (R⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
rw [abs_of_pos h]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
calc :
  Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
calc₁ :
  Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)
calc₂ : circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
calc₃ : log R + log⁺ (|R|⁻¹ * ‖c - a‖) = log R + log⁺ (R⁻¹ * ‖c - a‖)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
calc circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]

Premises used: Norm.norm, HMul.hMul, Real.posLog, abs, HSub.hSub, Complex.ofReal, Real.log, Inv.inv, HAdd.hAdd, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
pos : ∀ (hR : R = 0), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
neg : ∀ (hR : ¬R = 0), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R

Tactic:
by_cases hR : R = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : R = 0
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
neg : |R|⁻¹ * ‖c - a‖ ≤ 1
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R

Tactic:
rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left,
    posLog_eq_zero_iff, abs_mul, abs_inv, abs_of_nonneg (norm_nonneg (c - a))]

Premises used: circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, abs_inv, HSub.hSub, abs_mul, Real.posLog_eq_zero_iff, add_eq_left, abs_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ ‖c - a‖ ≤ |R|

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hu

Premises used: dist_eq_norm', Metric.mem_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
hu₁ : ‖c - a‖ ≤ |R|
⊢ ¬R = 0

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hu

Premises used: dist_eq_norm', Metric.mem_closedBall
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hu : ‖c - a‖ ≤ |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1

Tactic:
apply inv_mul_le_one_of_le₀ hu (abs_nonneg R)

Premises used: inv_mul_le_one_of_le₀, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
rw : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (1 + ‖x‖) 2
⊢ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 + ‖x‖

Tactic:
rw [sqrt_le_left (by positivity)]

Premises used: Real.sqrt_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ 1 + HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (1 + ‖x‖) 2

Tactic:
simp [add_sq]

Premises used: add_sq
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
rw : 1 + ‖x‖ ≤ √(2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2))
⊢ 1 + ‖x‖ ≤ √2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
rw [← sqrt_mul zero_le_two]

Premises used: Real.sqrt_mul, zero_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2

Tactic:
have := sq_nonneg (‖x‖ - 1)
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
this : 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2
h : HPow.hPow (β := ℕ) (1 + ‖x‖) 2 ≤ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ 1 + ‖x‖ ≤ √(2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2))

Tactic:
apply le_sqrt_of_sq_le

Premises used: Real.le_sqrt_of_sq_le
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
this : 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2
linarith :
  2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) < HPow.hPow (β := ℕ) (1 + ‖x‖) 2 →
    0 - HPow.hPow (β := ℕ) (‖x‖ - 1) 2 + (2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) - HPow.hPow (β := ℕ) (1 + ‖x‖) 2) = 0
⊢ HPow.hPow (β := ℕ) (1 + ‖x‖) 2 ≤ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
h : √2 ^ r ≠ 0
hx : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hx₁ : 0 ≤ √2
hy : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hx₂ : LE.le (α := ℝ) 0 2
hx₃ : 0 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹

Tactic:
rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]

Premises used: mul_inv_cancel_left₀, mul_inv, Real.mul_rpow, Real.rpow_div_two_eq_sqrt, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ √2 ^ r ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ √2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
hbc : 1 + ‖x‖ ≤ √2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹ ≤
    HPow.hPow (α := ℝ) 2 (r / 2) * ((1 + ‖x‖) ^ r)⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 1 + ‖x‖ ≤ √2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
apply one_add_norm_le_sqrt_two_mul_sqrt

Premises used: one_add_norm_le_sqrt_two_mul_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
hx : 0 ≤ 1 + ‖x‖
⊢ HPow.hPow (α := ℝ) 2 (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
rw [rpow_neg]

Premises used: Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
rw : t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1

Tactic:
rw [le_sub_iff_add_le', neg_inv]

Premises used: le_sub_iff_add_le', neg_inv
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ 0 < 1 + ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹

Tactic:
exact (Real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm

Premises used: Iff.mpr, Real.le_rpow_inv_iff_of_neg, neg_lt_zero, Iff.symm
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
rw : t ^ (-r⁻¹) < 1
⊢ Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) ∅

Tactic:
rw [Metric.closedBall_eq_empty, sub_neg]

Premises used: sub_neg, Metric.closedBall_eq_empty
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ -r⁻¹ < 0

Tactic:
simp only [hr, Right.neg_neg_iff, inv_pos]

Premises used: inv_pos, Right.neg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1

Tactic:
exact Real.rpow_lt_one_of_one_lt_of_neg ht (by simp only [hr, Right.neg_neg_iff, inv_pos])

Premises used: Real.rpow_lt_one_of_one_lt_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
⊢ 0 < r

Tactic:
have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
h : 0 ≤ x ^ (-r⁻¹) - 1
h₁ : LE.le (α := ℝ) 0 1
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
h : 1 ≤ x ^ (-r⁻¹)
⊢ 0 ≤ x ^ (-r⁻¹) - 1

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ -r⁻¹ ≤ 0

Tactic:
simpa using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ 1 ≤ x ^ (-r⁻¹)

Tactic:
exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)

Premises used: Real.one_le_rpow_of_pos_of_le_one_of_nonpos, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n) = ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))

Tactic:
simp [rpow_mul hx.1.le, ← neg_mul]

Premises used: LT.lt.le, And.left, neg_mul, Real.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
rw : ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)
rw₁ : ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n) = ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))

Tactic:
calc
      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
        gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp
      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]

Premises used: ENNReal.ofReal, HSub.hSub, Inv.inv, HPow.hPow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
⊢ ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))

Tactic:
have h_int x (hx : x ∈ Ioc (0 : ℝ) 1) := by
    calc
      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
        gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp
      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ∞

Tactic:
lt_of_le_of_lt (setLIntegral_mono' measurableSet_Ioc h_int) ?_

Premises used: lt_of_le_of_lt, measurableSet_Ioc, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
refine : ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ)))) < ∞
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ∞

Tactic:
refine lt_of_le_of_lt (setLIntegral_mono' measurableSet_Ioc h_int) ?_

Premises used: lt_of_le_of_lt, measurableSet_Ioc, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ)))) < ∞

Tactic:
IntegrableOn.setLIntegral_lt_top ?_

Premises used: MeasureTheory.IntegrableOn.setLIntegral_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
refine :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) (Ioc 0 1) volume
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ)))) < ∞

Tactic:
refine IntegrableOn.setLIntegral_lt_top ?_

Premises used: MeasureTheory.IntegrableOn.setLIntegral_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) volume 0 1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) (Ioc 0 1) volume

Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
h : -1 < -(r⁻¹ * (↑n : ℝ))
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) volume 0 1

Tactic:
apply intervalIntegral.intervalIntegrable_rpow'

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
h : r⁻¹ * (↑n : ℝ) < 1
h₁ : (↑n : ℝ) < 1 * r
h₂ h₃ h₄ h₅ : (↑n : ℝ) < r
⊢ -1 < -(r⁻¹ * (↑n : ℝ))

Tactic:
rwa [neg_lt_neg_iff, inv_mul_lt_iff₀' hr, one_mul]

Premises used: neg_lt_neg_iff, inv_mul_lt_iff₀', one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ 0 < r

Tactic:
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)

Tactic:
have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) := by fun_prop