awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
e_s : r < |x| ↔ 2 < 2 * r⁻¹ * |x|
e_s₁ : r < |x| ↔ 2 < 2 * (r⁻¹ * |x|)
⊢ r < |x| ↔ 2 < 2 * |r⁻¹| * |x|
have e_s₂ : r < |x| ↔ HMul.hMul (α := ℝ) 2⁻¹ 2 < r⁻¹ * |x|
Tactic: rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
e_s : r < |x| ↔ 2 < 2 * r⁻¹ * |x|
e_s₁ : r < |x| ↔ 2 < 2 * (r⁻¹ * |x|)
e_s₂ : r < |x| ↔ HMul.hMul (α := ℝ) 2⁻¹ 2 < r⁻¹ * |x|
⊢ r < |x| ↔ 2 < 2 * |r⁻¹| * |x|
have e_s₃ : r < |x| ↔ 1 < r⁻¹ * |x|
Tactic: rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
e_s : r < |x| ↔ 2 < 2 * r⁻¹ * |x|
e_s₁ : r < |x| ↔ 2 < 2 * (r⁻¹ * |x|)
e_s₂ : r < |x| ↔ HMul.hMul (α := ℝ) 2⁻¹ 2 < r⁻¹ * |x|
e_s₃ : r < |x| ↔ 1 < r⁻¹ * |x|
⊢ r < |x| ↔ 2 < 2 * |r⁻¹| * |x|
have e_s₄ : r < |x| ↔ r * 1 < |x|
Tactic: rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
e_s : r < |x| ↔ 2 < 2 * r⁻¹ * |x|
e_s₁ : r < |x| ↔ 2 < 2 * (r⁻¹ * |x|)
e_s₂ : r < |x| ↔ HMul.hMul (α := ℝ) 2⁻¹ 2 < r⁻¹ * |x|
e_s₃ : r < |x| ↔ 1 < r⁻¹ * |x|
e_s₄ : r < |x| ↔ r * 1 < |x|
⊢ r < |x| ↔ 2 < 2 * |r⁻¹| * |x|
have e_s₅ : r < |x| ↔ r < |x|
Tactic: rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
have rw : Eq (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ)
  (∫ (a : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, HMul.hMul (α := ℝ) 2 2⁻¹ ∂μ)
Tactic: rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ)
    (∫ (a : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, HMul.hMul (α := ℝ) 2 2⁻¹ ∂μ)
have e_f : ∀ (x : ℝ), 1 = HMul.hMul (α := ℝ) 2 2⁻¹
Tactic: congr with _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ 1 = HMul.hMul (α := ℝ) 2 2⁻¹
have e_f : Eq (α := ℝ) 1 1
Tactic: rw [mul_inv_cancel₀ (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ) ≤
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
have hbc : LE.le (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
  (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
Tactic: gcongr (2 : ℝ) * ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
    (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
have hbc : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) {x : ℝ | 2 < |2 * r⁻¹ * x|} μ
Tactic: refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
hbc : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) {x : ℝ | 2 < |2 * r⁻¹ * x|} μ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
    (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
have hbc₁ : MeasurableSet (α := ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|}
Tactic: refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
hbc : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) {x : ℝ | 2 < |2 * r⁻¹ * x|} μ
hbc₁ : MeasurableSet (α := ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|}
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
    (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
have hbc₂ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x), 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)
Tactic: refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) μ
have funProp : enorm (E := ℝ) 2⁻¹ ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ |2 * r⁻¹ * x|
have funProp : Real.measurableSpace ≤ Real.measurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
funProp : Real.measurableSpace ≤ Real.measurableSpace
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ |2 * r⁻¹ * x|
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x3 : ℝ) ↦ |x3|
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (hypothesis)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
hx0 : 2 * r⁻¹ * x = 0
⊢ False
have hx₁ : LT.lt (α := ℝ) 2 0
Tactic: simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx0 : 2 * r⁻¹ * x = 0
hx : LT.lt (α := ℝ) 2 0
⊢ False
have linarith : HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx0 : 2 * r⁻¹ * x = 0
hx : LT.lt (α := ℝ) 2 0
linarith linarith₁ : HMul.hMul (α := ℝ) 1 1 = 1
⊢ False
have linarith₂ : HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx0 : 2 * r⁻¹ * x = 0
hx : LT.lt (α := ℝ) 2 0
linarith linarith₁ : HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ : HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
⊢ False
have linarith₃ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (hypothesis)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)
have hx_ne : 2 * r⁻¹ * x ≠ 0
Tactic: have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
        linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
hx_ne : 2 * r⁻¹ * x ≠ 0
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)
have hbc : sinc (2 * r⁻¹ * x) ≤ HSub.hSub (α := ℝ) 1 2⁻¹
Tactic: rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
hx_ne : 2 * r⁻¹ * x ≠ 0
⊢ sinc (2 * r⁻¹ * x) ≤ HSub.hSub (α := ℝ) 1 2⁻¹
have hbc : sinc (2 * r⁻¹ * x) ≤ 1 / 2
Tactic: norm_num
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
hx_ne : 2 * r⁻¹ * x ≠ 0
⊢ sinc (2 * r⁻¹ * x) ≤ 1 / 2
have hbc : sinc (2 * r⁻¹ * x) ≤ 2⁻¹
Tactic: rw [one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
hx_ne : 2 * r⁻¹ * x ≠ 0
⊢ sinc (2 * r⁻¹ * x) ≤ 2⁻¹
have hbc : |2 * r⁻¹ * x|⁻¹ ≤ 2⁻¹
Tactic: refine (sinc_le_inv_abs hx_ne).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 1 - sinc (2 * r⁻¹ * x)) μ
have funProp : enorm (E := ℝ) 1 ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ) ≤
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
have grw : ∀ (x : ℝ), 0 x ≤ 1 - sinc (2 * r⁻¹ * x)
Tactic: grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ 0 x ≤ 1 - sinc (2 * r⁻¹ * x)
have simp : sinc (2 * r⁻¹ * x) ≤ 1
Tactic: simp only [Pi.zero_apply, sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ HMul.hMul (α := ℝ) 2 (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) ≤
    2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
have hbc : ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ ≤ Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * ‖2 * (↑r : ℂ)⁻¹ + 2 * (↑r⁻¹ : ℂ) - 2 * (2 * (↑r⁻¹ : ℂ)) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖
have norm_cast : 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
  2⁻¹ * r * ‖2 * r⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * ‖2 * r⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ‖
have rw : 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
  2⁻¹ * r * 2 * (2 * r⁻¹) * ‖HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖
Tactic: rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * 2 * (2 * r⁻¹) * ‖HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖
have e_a : 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
e_a : 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)
⊢ 2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * 2 * (2 * r⁻¹) * ‖HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖
have e_a₁ : ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ = HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)
have e_a : 2 = r * r⁻¹ * 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2 = r * r⁻¹ * 2
have e_a : 2 = HMul.hMul (α := ℝ) 1 2
Tactic: rw [mul_inv_cancel₀ (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
e_a : 2 = HMul.hMul (α := ℝ) 1 2
⊢ 2 = r * r⁻¹ * 2
have e_a₁ : Eq (α := ℝ) 2 2
Tactic: rw [mul_inv_cancel₀ (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ = HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)
have e_a : HSub.hSub (α := ℝ) (∫ (a : ℝ), 1 ∂μ) (∫ (a : ℝ), sinc (2 * r⁻¹ * a) ∂μ) =
  HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)
Tactic: rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 2⁻¹ * r * ‖2 * (↑r : ℂ)⁻¹ + 2 * (↑r⁻¹ : ℂ) - 2 * (2 * (↑r⁻¹ : ℂ)) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖ =
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have rw : 2⁻¹ * r * ‖2 * (↑r : ℂ)⁻¹ + 2 * (↑r⁻¹ : ℂ) - 2 * (2 * (↑r⁻¹ : ℂ)) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖ =
  2⁻¹ * r * ‖(∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1) - 2 * (↑(2 * r⁻¹) : ℂ) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖
Tactic: rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have calc : μ.real {x : ℝ | r < |x|} = μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|}
Tactic: calc μ.real {x | r < |x|}
  _ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
    congr 1 with x
    simp only [Set.mem_setOf_eq, abs_mul, Nat.abs_ofNat]
    rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
  _ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
  _ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ := by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]
  _ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
  _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
    simp only [Pi.zero_apply, sub_nonneg]
    exact sinc_le_one (2 * r⁻¹ * x)
  _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
    gcongr
    exact Real.le_norm_self _
  _ = 2⁻¹ * r *
      ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ := by
    norm_cast
    rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
    congr
    · ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]
    · rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp
  _ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ := by
    rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
calc : μ.real {x : ℝ | r < |x|} = μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|}
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have calc₁ : μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ
Tactic: calc μ.real {x | r < |x|}
  _ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
    congr 1 with x
    simp only [Set.mem_setOf_eq, abs_mul, Nat.abs_ofNat]
    rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
  _ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
  _ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ := by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]
  _ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
  _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
    simp only [Pi.zero_apply, sub_nonneg]
    exact sinc_le_one (2 * r⁻¹ * x)
  _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
    gcongr
    exact Real.le_norm_self _
  _ = 2⁻¹ * r *
      ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ := by
    norm_cast
    rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
    congr
    · ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]
    · rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp
  _ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ := by
    rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
    simp