mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
⊢ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a) = ((b - a) / 2) ^ 2 - (∫ (x : Ω), X x ∂μ - (b + a) / 2) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᵐ[μ i] Y i
hZT : Z =ᵐ[μ'] T
h : TendstoInDistribution X l Z μ μ'
⊢ Tendsto (fun n ↦ ⟨Measure.map (Y n) (μ n), ⋯⟩) l (𝓝 ⟨Measure.map T μ', ⋯⟩)

Tactic:
by
    convert! h.tendsto using 2 with n
    · simpa using Measure.map_congr (hXY n).symm
    · rw! [Measure.map_congr hZT]
      rfl

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_5
𝓧 : Type u_6
m mΩ : MeasurableSpace Ω
P : Measure Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
A : Set Ω
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ mΩ
f : 𝓧 → E
hA1 : Indep m (MeasurableSpace.comap X m𝓧) P
hX : AEMeasurable X P
hA2 : MeasurableSet A
hf : AEStronglyMeasurable f (Measure.map X P)
⊢ ∫ (ω : Ω) in A, f (X ω) ∂P = ∫ (ω : Ω), id (A.indicator 1 ω) • f (X ω) ∂P

Tactic:
by
        rw [← integral_indicator (hm A hA2)]
        congr with ω
        by_cases hω : ω ∈ A <;> simp [hω]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ μ''.real {x | ‖Y n x - X n x‖ < ε / 2} * (↑L * (ε / 2)) + μ''.real {x | ε / 2 ≤ ‖Y n x - X n x‖} * M =
    ↑L * (ε / 2) * μ''.real {x | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {x | ε / 2 ≤ ‖Y n x - X n x‖}

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ eLpNorm f p (dirac i) = ‖f i‖ₑ

Tactic:
eLpNorm,

Goal state after:
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f (dirac i) else eLpNorm' f p.toReal (dirac i)) = ‖f i‖ₑ
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case e_a.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ -(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2 = (circleMap z R x✝ - w) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
⊢ modularCharacterFun g = (map (fun x ↦ x * g) μ).haarScalarFactor μ

Tactic:
by
  let ν := MeasureTheory.Measure.haar (G := G)
  obtain ⟨⟨f, f_cont⟩, f_comp, f_nonneg, f_one⟩ :
    ∃ f : C(G, ℝ), HasCompactSupport f ∧ 0 ≤ f ∧ f 1 ≠ 0 := exists_continuous_nonneg_pos 1
  have int_f_ne_zero (μ₀ : Measure G) [IsHaarMeasure μ₀] : ∫ x, f x ∂μ₀ ≠ 0 :=
    ne_of_gt (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_one)
  apply NNReal.coe_injective
  have t : (∫ x, f (x * g) ∂ν) = (∫ x, f (x * g) ∂(haarScalarFactor ν μ • μ)) := by
    refine integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport ν μ ?_ ?_
    · exact Continuous.comp' f_cont (continuous_mul_const g)
    · have j : (fun x ↦ f (x * g)) = (f ∘ (Homeomorph.mulRight g)) := rfl
      rw [j]
      exact HasCompactSupport.comp_homeomorph f_comp _
  have r : (haarScalarFactor ν μ : ℝ) / (haarScalarFactor ν μ) = 1 := by
    refine div_self ?_
    rw [NNReal.coe_ne_zero]
    apply (ne_of_lt (haarScalarFactor_pos_of_isHaarMeasure _ _)).symm
  calc
  ↑(modularCharacterFun g) = ↑(haarScalarFactor (map (· * g) ν) ν) := by borelize G; rfl
  _ = (∫ x, f x ∂(map (· * g) ν)) / ∫ x, f x ∂ν :=
    haarScalarFactor_eq_integral_div _ _ f_cont f_comp (int_f_ne_zero ν)
  _ = (∫ x, f (x * g) ∂ν) / ∫ x, f x ∂ν := by
    rw [integral_map (AEMeasurable.mul_const aemeasurable_id' _)
    (Continuous.aestronglyMeasurable f_cont)]
  _ = (∫ x, f (x * g) ∂(haarScalarFactor ν μ • μ)) / ∫ x, f x ∂ν := by rw [t]
  _ = (∫ x, f (x * g) ∂(haarScalarFactor ν μ • μ)) / ∫ x, f x ∂(haarScalarFactor ν μ • μ) := by
    rw [integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport ν μ f_cont f_comp]
  _ = (haarScalarFactor ν μ • ∫ x, f (x * g) ∂μ) / (haarScalarFactor ν μ • ∫ x, f x ∂μ) := by
    rw [integral_smul_nnreal_measure, integral_smul_nnreal_measure]
  _ = (haarScalarFactor ν μ / haarScalarFactor ν μ) * ((∫ x, f (x * g) ∂μ) / ∫ x, f x ∂μ) :=
    mul_div_mul_comm _ _ _ _
  _ = 1 * ((∫ x, f (x * g) ∂μ) / ∫ x, f x ∂μ) := by rw [r]
  _ = (∫ x, f (x * g) ∂μ) / ∫ x, f x ∂μ := by rw [one_mul]
  _ = (∫ x, f x ∂(map (· * g) μ)) / ∫ x, f x ∂μ := by
    rw [integral_map (AEMeasurable.mul_const aemeasurable_id' _)
    (Continuous.aestronglyMeasurable f_cont)]
  _ = haarScalarFactor (map (· * g) μ) μ :=
    (haarScalarFactor_eq_integral_div _ _ f_cont f_comp (int_f_ne_zero μ)).symm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have := IsCompact.exists_isMaxOn comp none (cts.mono <| prod_mono_right (subset_univ _))

Goal state after:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ 1 / p - 1 + q / p = (q + 1) / p - 1

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ f.nnrealPart) + ↑(Λ g.nnrealPart) - (↑(Λ (-f).nnrealPart) + ↑(Λ (-g).nnrealPart)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ b ^ (p⁻¹ * -1) * b ^ (-p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 ≤ b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p

Tactic:
← rpow_add

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 ≤ b

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a.e_a
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ p⁻¹ * -1 + -p⁻¹ * q = -(q + 1) / p

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ -a * ↑(Λ (-f).nnrealPart) - -a * ↑(Λ f.nnrealPart) = a * (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_7
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x✝ : ℝ × ℝ
⊢ x✝.1 * (|x✝.1| ^ q * rexp (-|x✝.1| ^ p)) = x✝.1 * |x✝.1| ^ q * rexp (-|x✝.1| ^ p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-x ^ p) = x ^ q * x * rexp (-x ^ p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + (1 + 1)) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
one_add_one_eq_two

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 2) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 2) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_7
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x✝ : ℝ × ℝ
⊢ x✝.1 * (|x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)) = x✝.1 * |x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + (1 + 1)) / p) * (1 / p) * Real.Gamma ((q + (1 + 1)) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
one_add_one_eq_two

Goal state after:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case e_a.e_t
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ 1 - 2 * (1 - t) = 2 * t - 1

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι b a), 0 ≤ g x

Tactic:
uIoc_comm

Goal state after:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
t : ℝ
ht : t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
ht_mem : t ∈ Ioo 0 1
⊢ ‖deriv g t‖ ≤ C

Tactic:
by simpa only [(hdg t ht_mem).deriv] using ht ht_mem

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ ddg y = 1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ x ∈ Set.Icc a b, |ddg x| ≤ ζ / 2 * (x - a) ^ 1
key :
  ∀ {φ φ' : ℝ → ℝ},
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) →
      φ a = 0 →
        ∀ {c : ℝ} {n : ℕ},
          (∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n) → ∀ t ∈ Set.Icc a b, |φ t| ≤ c / (↑n + 1) * (t - a) ^ (n + 1)
⊢ dg a = 0

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ↑(NNReal.mk (∫ (x : X), ↑(f x) ∂rieszMeasure Λ) ⋯) = ↑(Λ f)

Tactic:
NNReal.coe_mk

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : (Fin 0 → ℂ) → E
c : Fin 0 → ℂ
R : Fin 0 → ℝ
⊢ (∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c

Tactic:
by
  simp only [torusIntegral, Fin.prod_univ_zero, one_smul,
    Subsingleton.elim (fun _ : Fin 0 => 2 * π) 0, Icc_self, Measure.restrict_singleton, volume_pi,
    integral_dirac, Measure.pi_of_empty (fun _ : Fin 0 ↦ volume) 0,
    Measure.dirac_apply_of_mem (mem_singleton _), Subsingleton.elim (torusMap c R 0) c]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
n : ℕ
⊢ invariants f ≤ invariants f^[n]

Tactic:
induction n with
  | zero => simp [invariants_le]
  | succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
⊢ ContDiff ℝ (↑n) (charFun μ)

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
⊢ ContDiff ℝ ↑n fun x ↦ fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k) μ
⊢ ContDiff ℝ (↑n) (charFun μ)

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k) μ
⊢ ContDiff ℝ ↑n fun x ↦ fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (iteratedFDeriv ℝ n (charFun μ) t) x = I ^ n * ∫ (y : E), ↑(∏ i, ⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (iteratedFDeriv ℝ n (fun x ↦ fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)) t) x =
    I ^ n * ∫ (y : E), ↑(∏ i, ⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: case hf
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ContDiff ℝ (↑n) (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 1)

Tactic:
exact contDiff_fourierIntegral _ hint'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
x✝ : E
⊢ cexp (I * ↑⟪x✝, t⟫) * ∏ i, ↑⟪x✝, x i⟫ = (∏ i, ↑⟪x✝, x i⟫) * cexp (I * ↑⟪x✝, t⟫)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (Measure.map X P)
⊢ (1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I) * 2 - ↑t ^ 2 * ↑(∫ (x : Ω), X x ^ 2 ∂P) =
    (1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I) * 2 + -(↑t ^ 2 * ↑(∫ (x : Ω), X x ^ 2 ∂P))

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case e_f
E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t a : E
⊢ (↑⟪a, t⟫ + ↑⟪r, t⟫) * I = ↑⟪a, t⟫ * I + ↑⟪r, t⟫ * I

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
⊢ ν = Measure.pi μ

Tactic:
refine (MeasurableEquiv.toLp 2 (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_
    rw [MeasurableEquiv.coe_toLp, h, charFun_pi]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case e_f
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ (↑(L a) + ↑(L r)) * I = ↑(L a) * I + ↑(L r) * I

Tactic:
ring

Goal state after: