awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
h : (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
neg : ∫ (x : ℝ) in -r..r, cexp ((↑(x * y) : ℂ) * I) = (↑(y⁻¹ * y) : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑(y * x) : ℂ) * I)
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
    (↑y : ℂ)⁻¹ * (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
h : (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑(x * y) : ℂ) * I) = (↑(y⁻¹ * y) : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑(y * x) : ℂ) * I)

Tactic:
simp [mul_comm _ y, mul_inv_cancel₀ hy]

Premises used: mul_inv_cancel₀, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
e_f :
  ∀ (y : ℝ),
    (if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)) =
      2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)
⊢ Eq (α := ℂ)
    (∫ (y : ℝ), if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I) ∂μ)
    (∫ (x : ℝ), 2 * (↑r : ℂ) * (↑(sinc (r * x)) : ℂ) ∂μ)

Tactic:
congr with y
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
e_f :
  (if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * (2 * (↑(y * r) : ℂ) * (↑(sinc (y * r)) : ℂ))) =
    2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)
⊢ (if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)) =
    2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)

Tactic:
rw [integral_exp_mul_I_eq_sinc]

Premises used: integral_exp_mul_I_eq_sinc
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
pos : ∀ (hry : r * y = 0), 2 * (↑r : ℂ) = 2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)
neg :
  ∀ (hry : ¬r * y = 0), (↑y⁻¹ : ℂ) * (2 * (↑(y * r) : ℂ) * (↑(sinc (y * r)) : ℂ)) = 2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)
⊢ (if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * (2 * (↑(y * r) : ℂ) * (↑(sinc (y * r)) : ℂ))) =
    2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)

Tactic:
split_ifs with hry
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hry : r * y = 0
⊢ 2 * (↑r : ℂ) = 2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)

Tactic:
simp [hry]
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hry : ¬r * y = 0
hy : y = 0
⊢ r * y = 0

Tactic:
simp [hy]
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hry : ¬r * y = 0
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := fun hy ↦ hry (by simp [hy])
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hry : ¬r * y = 0
hy : y ≠ 0
neg : y⁻¹ * (2 * (y * r) * sinc (y * r)) = 2 * r * sinc (r * y)
⊢ (↑y⁻¹ : ℂ) * (2 * (↑(y * r) : ℂ) * (↑(sinc (y * r)) : ℂ)) = 2 * (↑r : ℂ) * (↑(sinc (r * y)) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hry : ¬r * y = 0
hy : y ≠ 0
⊢ y⁻¹ * (2 * (y * r) * sinc (y * r)) = 2 * r * sinc (r * y)

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
norm_cast : ∫ (x : ℝ), 2 * r * sinc (r * x) ∂μ = 2 * r * ∫ (x : ℝ), sinc (r * x) ∂μ
⊢ ∫ (x : ℝ), 2 * (↑r : ℂ) * (↑(sinc (r * x)) : ℂ) ∂μ = 2 * (↑r : ℂ) * (↑(∫ (x : ℝ), sinc (r * x) ∂μ) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
rw rw₁ : Eq (α := ℝ) (∫ (x : ℝ), 2 * r * sinc (r * x) ∂μ) (∫ (a : ℝ), 2 * r * sinc (r * a) ∂μ)
⊢ ∫ (x : ℝ), 2 * r * sinc (r * x) ∂μ = 2 * r * ∫ (x : ℝ), sinc (r * x) ∂μ

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
calc : Eq (α := ℂ) (∫ (t : ℝ) in -r..r, charFun μ t) (∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
calc₁ :
  Eq (α := ℂ) (∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
calc₂ :
  Eq (α := ℂ) (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I) ∂μ)
calc₃ :
  Eq (α := ℂ)
    (∫ (y : ℝ), if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I) ∂μ)
    (∫ (x : ℝ), 2 * (↑r : ℂ) * (↑(sinc (r * x)) : ℂ) ∂μ)
calc₄ : ∫ (x : ℝ), 2 * (↑r : ℂ) * (↑(sinc (r * x)) : ℂ) ∂μ = 2 * (↑r : ℂ) * (↑(∫ (x : ℝ), sinc (r * x) ∂μ) : ℂ)
⊢ ∫ (t : ℝ) in -r..r, charFun μ t = 2 * (↑r : ℂ) * (↑(∫ (x : ℝ), sinc (r * x) ∂μ) : ℂ)

Tactic:
calc ∫ t in -r..r, charFun μ t
  _ = ∫ x in -r..r, ∫ y, cexp (x * y * I) ∂μ := by simp_rw [charFun_apply_real]
  _ = ∫ y, ∫ x in -r..r, cexp (x * y * I) ∂volume ∂μ := by
    rw [intervalIntegral_integral_swap h_int]
  _ = ∫ y, if r * y = 0 then 2 * (r : ℂ)
      else y⁻¹ * ∫ x in -(y * r)..y * r, cexp (x * I) ∂volume ∂μ := by
    congr with y
    by_cases hy : y = 0
    · simp [hy, two_mul]
    simp only [mul_eq_zero, hr.ne', hy, or_self, ↓reduceIte, ofReal_inv]
    have h := intervalIntegral.integral_deriv_smul_comp (E := ℂ) (a := -r) (b := r)
      (f := fun x ↦ y * x) (f' := fun _ ↦ y) (g := fun x ↦ cexp (x * I)) ?_ (by fun_prop)
      (by fun_prop)
    swap
    · intro x hx
      simp_rw [mul_comm y]
      exact hasDerivAt_mul_const _
    simp only [Function.comp_apply, ofReal_mul, real_smul, intervalIntegral.integral_const_mul,
      mul_neg] at h
    rw [← h, ← mul_assoc]
    norm_cast
    simp [mul_comm _ y, mul_inv_cancel₀ hy]
  _ = ∫ x, 2 * (r : ℂ) * sinc (r * x) ∂μ := by
    congr with y
    rw [integral_exp_mul_I_eq_sinc]
    split_ifs with hry
    · simp [hry]
    have hy : y ≠ 0 := fun hy ↦ hry (by simp [hy])
    norm_cast
    field_simp
  _ = 2 * r * ∫ x, sinc (r * x) ∂μ := by
    norm_cast
    rw [← integral_const_mul]

Premises used: Complex.ofReal, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r_1 : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r_1
r : ℝ
⊢ AEMeasurable (HMul.hMul r) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
⊢ ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ

Tactic:
have integrable_sinc_const_mul (r : ℝ) : Integrable (fun x ↦ sinc (r * x)) μ :=
    (integrable_map_measure stronglyMeasurable_sinc.aestronglyMeasurable (by fun_prop)).mp
      integrable_sinc
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
e_s :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | r < |x|} x ↔ Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x
⊢ μ.real {x : ℝ | r < |x|} = μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|}

Tactic:
congr 1 with x
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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|
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | r < |x|} x ↔ Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x

Tactic:
simp only [Set.mem_setOf_eq, abs_mul, Nat.abs_ofNat]

Premises used: abs_mul, Set.mem_setOf_eq, Nat.abs_ofNat
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ 0 ≤ r⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ LT.lt (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ Ne (α := ℝ) 2 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ 0 < r

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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|
e_s₅ e_s₆ : r < |x| ↔ r < |x|
⊢ r < |x| ↔ 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]

Premises used: mul_assoc, inv_mul_lt_iff₀, lt_inv_mul_iff₀, abs_of_nonneg, mul_one, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ)
    (∫ (a : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, HMul.hMul (α := ℝ) 2 2⁻¹ ∂μ)
⊢ ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
e_f : ∀ (x : ℝ), 1 = HMul.hMul (α := ℝ) 2 2⁻¹
⊢ Eq (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ)
    (∫ (a : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, HMul.hMul (α := ℝ) 2 2⁻¹ ∂μ)

Tactic:
congr with _
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
e_f e_f₁ : Eq (α := ℝ) 1 1
⊢ 1 = HMul.hMul (α := ℝ) 2 2⁻¹

Tactic:
rw [mul_inv_cancel₀ (by positivity)]

Premises used: mul_inv_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
hbc :
  LE.le (α := ℝ) (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
    (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * 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) ∂μ)

Tactic:
gcongr (2 : ℝ) * ?_

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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) ∂μ)

Tactic:
setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_on, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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|}
hbc₂ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|} x), 2⁻¹ ≤ 1 - sinc (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) ∂μ)

Tactic:
refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_on, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
funProp : enorm (E := ℝ) 2⁻¹ ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹) {x : ℝ | 2 < |2 * r⁻¹ * x|} μ

Tactic:
exact Integrable.integrableOn <| by fun_prop

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
funProp : Real.measurableSpace ≤ Real.measurableSpace
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x3 : ℝ) ↦ |x3|
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ |2 * r⁻¹ * x|

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ MeasurableSet (α := ℝ) {x : ℝ | 2 < |2 * r⁻¹ * x|}

Tactic:
exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

Premises used: MeasurableSet.preimage, measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
⊢ LT.lt (α := ℝ) 2 0

Tactic:
simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx

Premises used: Set.mem_setOf_eq, abs_zero
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
linarith₃ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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 * 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
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
hbc : sinc (2 * r⁻¹ * x) ≤ HSub.hSub (α := ℝ) 1 2⁻¹
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)

Tactic:
rw [le_sub_iff_add_le, ← le_sub_iff_add_le']

Premises used: le_sub_iff_add_le', le_sub_iff_add_le
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
hbc : sinc (2 * r⁻¹ * x) ≤ 1 / 2
⊢ sinc (2 * r⁻¹ * x) ≤ HSub.hSub (α := ℝ) 1 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
hbc : sinc (2 * r⁻¹ * x) ≤ 2⁻¹
⊢ sinc (2 * r⁻¹ * x) ≤ 1 / 2

Tactic:
rw [one_div]

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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⁻¹

Tactic:
(sinc_le_inv_abs hx_ne).trans ?_

Premises used: LE.le.trans, Real.sinc_le_inv_abs
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
hbc : |2 * r⁻¹ * x|⁻¹ ≤ 2⁻¹
⊢ sinc (2 * r⁻¹ * x) ≤ 2⁻¹

Tactic:
refine (sinc_le_inv_abs hx_ne).trans ?_

Premises used: LE.le.trans, Real.sinc_le_inv_abs
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
⊢ 0 < |2 * r⁻¹ * x|

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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
⊢ LT.lt (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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 * r⁻¹ * x|⁻¹ ≤ 2⁻¹

Tactic:
exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)

Premises used: Iff.mpr, le_of_lt, inv_le_inv₀
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
funProp : enorm (E := ℝ) 1 ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 1 - sinc (2 * r⁻¹ * x)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
grw : ∀ (x : ℝ), 0 x ≤ 1 - sinc (2 * 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) ∂μ)

Tactic:
grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]

Premises used: MeasureTheory.setIntegral_le_integral, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
simp : sinc (2 * r⁻¹ * x) ≤ 1
⊢ 0 x ≤ 1 - sinc (2 * r⁻¹ * x)

Tactic:
simp only [Pi.zero_apply, sub_nonneg]

Premises used: Pi.zero_apply, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ sinc (2 * r⁻¹ * x) ≤ 1

Tactic:
sinc_le_one (2 * r⁻¹ * x)

Premises used: HMul.hMul, Inv.inv, Real.sinc_le_one, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
x : ℝ
⊢ sinc (2 * r⁻¹ * x) ≤ 1

Tactic:
exact sinc_le_one (2 * r⁻¹ * x)

Premises used: HMul.hMul, Inv.inv, Real.sinc_le_one, OfNat.ofNat