awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ ≤ Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
⊢ HMul.hMul (α := ℝ) 2 (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) ≤
    2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)

Tactic:
gcongr
-- 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 : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ ≤ Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)

Tactic:
Real.le_norm_self _

Premises used: Real.le_norm_self
-- 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 : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ ≤ Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)

Tactic:
exact Real.le_norm_self _

Premises used: Real.le_norm_self
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
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) ∂μ‖
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ 0 ≤ 2 * 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)) μ
rw :
  2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * 2 * (2 * r⁻¹) * ‖HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * 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) ∂μ‖

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]

Premises used: mul_sub, mul_assoc, two_mul, mul_one_sub, norm_mul, OfNat.ofNat, Real.norm_ofNat, Real.norm_of_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)) μ
e_a : 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)
e_a₁ : ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ = HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * 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) ∂μ)‖

Tactic:
congr
-- 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_a : 2 = r * r⁻¹ * 2
⊢ 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
⊢ r ≠ 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)) μ
e_a : 2 = HMul.hMul (α := ℝ) 1 2
e_a₁ e_a₂ : Eq (α := ℝ) 2 2
⊢ 2 = r * r⁻¹ * 2

Tactic:
rw [mul_inv_cancel₀ (by positivity), one_mul]

Premises used: mul_inv_cancel₀, one_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_a :
  HSub.hSub (α := ℝ) (∫ (a : ℝ), 1 ∂μ) (∫ (a : ℝ), sinc (2 * r⁻¹ * a) ∂μ) =
    HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)
⊢ ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ = HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)

Tactic:
rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]

Premises used: MeasureTheory.integral_sub, 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)) μ
⊢ HSub.hSub (α := ℝ) (∫ (a : ℝ), 1 ∂μ) (∫ (a : ℝ), sinc (2 * r⁻¹ * a) ∂μ) =
    HSub.hSub (α := ℝ) 1 (∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)

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)) μ
⊢ 0 < 2 * 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)) μ
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) ∂μ) : ℂ)‖
⊢ 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)

Tactic:
rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]

Premises used: MeasureTheory.integral_charFun_Icc, intervalIntegral.integral_sub, intervalIntegrable_const, neg_mul, MeasureTheory.intervalIntegrable_charFun
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
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 * ‖(∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1) - 2 * (↑(2 * r⁻¹) : ℂ) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
⊢ IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
have : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map (by fun_prop)
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|} ≤
    2⁻¹ * r *
      Norm.norm (E := ℂ)
        (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) t)

Tactic:
measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr

Premises used: MeasureTheory.measureReal_abs_gt_le_integral_charFun
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
h :
  μ.real {x : E | r < |(L : (a : E) → ℝ) x|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|}
h₁ : ∀ (x : ℝ), charFunDual μ (x • L) = charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) x
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L))

Tactic:
convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x

Premises used: MeasureTheory.measureReal_abs_gt_le_integral_charFun
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Measurable (α := E) (β := ℝ) (⇑L : (a : E) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
h : μ.real {x : E | r < |(L : (a : E) → ℝ) x|} = μ.real (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) {x : ℝ | r < |x|})
h₁ : MeasurableSet (α := ℝ) {x : ℝ | r < |x|}
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|}

Tactic:
rw [map_measureReal_apply (by fun_prop)]

Premises used: MeasureTheory.map_measureReal_apply
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} = μ.real (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) {x : ℝ | r < |x|})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
funProp : Real.measurableSpace ≤ Real.measurableSpace
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : ℝ) ↦ |a|
⊢ Measurable (α := ℝ) abs

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ MeasurableSet (α := ℝ) {x : ℝ | r < |x|}

Tactic:
exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

Premises used: MeasurableSet.preimage, measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
x : ℝ
h h₁ : charFunDual μ (x • L) = charFunDual μ (x • L)
⊢ charFunDual μ (x • L) = charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) x

Tactic:
rw [charFun_map_eq_charFunDual_smul]

Premises used: MeasureTheory.charFun_map_eq_charFunDual_smul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ ⟪a, x⟫) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
⊢ IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)

Tactic:
have : IsProbabilityMeasure (μ.map (fun x ↦ ⟪a, x⟫)) :=
    Measure.isProbabilityMeasure_map (by fun_prop)
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
⊢ Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|} ≤
    2⁻¹ * r *
      Norm.norm (E := ℂ)
        (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹,
          1 - charFun (mE := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) t)

Tactic:
measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr

Premises used: MeasureTheory.measureReal_abs_gt_le_integral_charFun
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
h :
  μ.real {x : E | r < |⟪a, x⟫|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|}
h₁ : ∀ (x : ℝ), charFun μ (x • a) = charFun (mE := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) x
⊢ μ.real {x : E | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a))

Tactic:
convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr with x

Premises used: MeasureTheory.measureReal_abs_gt_le_integral_charFun
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
funProp : mE ≤ mE
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E) ↦ ⟪a, x⟫
⊢ Measurable (β := ℝ) fun (x : E) ↦ ⟪a, x⟫

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
h : μ.real {x : E | r < |⟪a, x⟫|} = μ.real (Set.preimage (β := ℝ) (fun (x : E) ↦ ⟪a, x⟫) {x : ℝ | r < |x|})
h₁ : MeasurableSet (α := ℝ) {x : ℝ | r < |x|}
⊢ μ.real {x : E | r < |⟪a, x⟫|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|}

Tactic:
rw [map_measureReal_apply (by fun_prop)]

Premises used: MeasureTheory.map_measureReal_apply
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
⊢ μ.real {x : E | r < |⟪a, x⟫|} = μ.real (Set.preimage (β := ℝ) (fun (x : E) ↦ ⟪a, x⟫) {x : ℝ | r < |x|})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
funProp : Real.measurableSpace ≤ Real.measurableSpace
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : ℝ) ↦ |a|
⊢ Measurable (α := ℝ) abs

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet (α := ℝ) {x : ℝ | r < |x|}

Tactic:
exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

Premises used: MeasurableSet.preimage, measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
x : ℝ
h :
  Eq (α := ℂ) (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪x_1, a⟫ : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) fun (x_1 : ℝ) ↦
      cexp ((↑x : ℂ) * (↑x_1 : ℂ) * I))
⊢ charFun μ (x • a) = charFun (mE := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) x

Tactic:
simp only [charFun_apply, inner_smul_right, conj_trivial, ofReal_mul, RCLike.inner_apply]

Premises used: MeasureTheory.charFun_apply, conj_trivial, RCLike.inner_apply, inner_smul_right, Complex.ofReal_mul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
x : ℝ
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ ⟪a, x⟫) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
x : ℝ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x_1 : ℝ) ↦ cexp ((↑x : ℂ) * (↑x_1 : ℂ) * I))
    (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
x : ℝ
h :
  Eq (α := ℂ) (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪x_1, a⟫ : ℂ) * I) ∂μ)
    (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪a, x_1⟫ : ℂ) * I) ∂μ)
⊢ Eq (α := ℂ) (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪x_1, a⟫ : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) fun (x_1 : ℝ) ↦
      cexp ((↑x : ℂ) * (↑x_1 : ℂ) * I))

Tactic:
rw [integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
μ : Measure E
inst_3 : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ)
x : ℝ
⊢ Eq (α := ℂ) (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪x_1, a⟫ : ℂ) * I) ∂μ)
    (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪a, x_1⟫ : ℂ) * I) ∂μ)

Tactic:
simp_rw [real_inner_comm a]

Premises used: real_inner_comm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
p q : ℚ
⊢ Eq (α := ℝ≥0∞) ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
    ((Measure.map (fun (x : ℝ) ↦ a + x) StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) :
      ℝ≥0∞)

Tactic:
simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo,
            sub_sub_sub_cancel_right, StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim,
            StieltjesFunction.id_apply, id, preimage_const_add_Ioo]

Premises used: sub_sub_sub_cancel_right, Set.preimage_const_add_Ioo, StieltjesFunction.measure_Ioo, MeasurableAdd.measurable_const_add, MeasureTheory.Measure.map_apply, StieltjesFunction.id_leftLim, id, measurableSet_Ioo, StieltjesFunction.id_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
⊢ IsAddLeftInvariant StieltjesFunction.id.measure

Tactic:
haveI : IsAddLeftInvariant StieltjesFunction.id.measure :=
    ⟨fun a =>
      Eq.symm <|
        Real.measure_ext_Ioo_rat fun p q => by
          simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo,
            sub_sub_sub_cancel_right, StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim,
            StieltjesFunction.id_apply, id, preimage_const_add_Ioo]⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
inl :
  ∀
    (H :
      Eq (α := Set ℝ)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ))
        (Icc 0 1)),
    Eq (α := ℝ≥0∞)
      ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
          (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
            (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
        ℝ≥0∞)
      (1 : ℝ≥0∞)
inr :
  ∀
    (H :
      Eq (α := Set ℝ)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ))
        (Icc (-1) 0)),
    Eq (α := ℝ≥0∞)
      ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
          (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
            (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
        ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H)

Premises used: Real, parallelepiped_orthonormalBasis_one_dim, stdOrthonormalBasis