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)) μ
calc : μ.real {x : ℝ | r < |x|} = μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|}
calc₁ : μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have calc₂ : ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
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|}
calc₁ : μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ
calc₂ :
  ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have calc₃ : 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: 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|}
calc₁ : μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ
calc₂ :
  ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
calc₃ :
  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) ∂μ)
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
have calc₄ : 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: 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 (hypothesis)
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
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L))
have this : IsProbabilityMeasure (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: have : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|} ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L))
have h : μ.real {x : E | r < |(L : (a : E) → ℝ) x|} =
  Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|}
Tactic: convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|}
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L))
have h₁ : ∀ (x : ℝ), charFunDual μ (x • L) = charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) x
Tactic: convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|}
have h : μ.real {x : E | r < |(L : (a : E) → ℝ) x|} = μ.real (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) {x : ℝ | r < |x|})
Tactic: rw [map_measureReal_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|})
⊢ μ.real {x : E | r < |(L : (a : E) → ℝ) x|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) {x : ℝ | r < |x|}
have h₁ : MeasurableSet (α := ℝ) {x : ℝ | r < |x|}
Tactic: rw [map_measureReal_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 (α := ℝ) abs
have funProp : Real.measurableSpace ≤ Real.measurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
⊢ Measurable (α := ℝ) abs
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : ℝ) ↦ |a|
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 : ℝ
⊢ charFunDual μ (x • L) = charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) x
have h : charFunDual μ (x • L) = charFunDual μ (x • L)
Tactic: rw [charFun_map_eq_charFunDual_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (hypothesis)
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
⊢ μ.real {x : E | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a))
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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⟫|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a))
have h : μ.real {x : E | r < |⟪a, x⟫|} =
  Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|}
Tactic: convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|}
⊢ μ.real {x : E | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a))
have h₁ : ∀ (x : ℝ), charFun μ (x • a) = charFun (mE := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) x
Tactic: convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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⟫) μ)
⊢ Measurable (β := ℝ) fun (x : E) ↦ ⟪a, x⟫
have funProp : mE ≤ mE
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
⊢ Measurable (β := ℝ) fun (x : E) ↦ ⟪a, x⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E) ↦ ⟪a, x⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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⟫|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|}
have h : μ.real {x : E | r < |⟪a, x⟫|} = μ.real (Set.preimage (β := ℝ) (fun (x : E) ↦ ⟪a, x⟫) {x : ℝ | r < |x|})
Tactic: rw [map_measureReal_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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|})
⊢ μ.real {x : E | r < |⟪a, x⟫|} =
    Measure.real (α := ℝ) (m := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) {x : ℝ | r < |x|}
have h₁ : MeasurableSet (α := ℝ) {x : ℝ | r < |x|}
Tactic: rw [map_measureReal_apply (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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⟫) μ)
⊢ Measurable (α := ℝ) abs
have funProp : Real.measurableSpace ≤ Real.measurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
⊢ Measurable (α := ℝ) abs
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : ℝ) ↦ |a|
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 : ℝ
⊢ charFun μ (x • a) = charFun (mE := Real.measurableSpace) (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) x
have 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))
Tactic: simp only [charFun_apply, inner_smul_right, conj_trivial, ofReal_mul, RCLike.inner_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : E) ↦ ⟪a, x⟫) μ) fun (x_1 : ℝ) ↦
      cexp ((↑x : ℂ) * (↑x_1 : ℂ) * I))
have h : Eq (α := ℂ) (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪x_1, a⟫ : ℂ) * I) ∂μ)
  (∫ (x_1 : E), cexp ((↑x : ℂ) * (↑⟪a, x_1⟫ : ℂ) * I) ∂μ)
Tactic: rw [integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
⊢ Eq (α := Measure ℝ) volume StieltjesFunction.id.measure
have this : 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]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have 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∞)
Tactic: rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H)