mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)

pp: case e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)

Tactic:
·

Goal state after:
case e'_2
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

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

Tactic:
·

Goal state after:
case e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

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

Tactic:
Gamma_add_one (one_div_ne_zero (ne_of_gt hp)),

Goal state after:
case e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
·

Goal state after:
case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
inst✝ : ⊥.IsCountablyGenerated
As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))

pp: case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
inst✝ : ⊥.IsCountablyGenerated
As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case inl
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst✝ : ⊥.IsCountablyGenerated
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))

pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst✝ : ⊥.IsCountablyGenerated
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
⊢ 2 • I =ᶠ[𝓝 (2 * t)] I

Tactic:
rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]

Goal state after:
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inl
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : t < 0
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

pp: case inr.inl
𝕜 : 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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 0] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * 0) = 𝓝[I] (2 * 0)

pp: case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
·

Goal state after:
case inl
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : t < 0
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inr.inl
𝕜 : 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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 0] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * 0) = 𝓝[I] (2 * 0)

pp: case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
·

Goal state after:
case inr.inl
𝕜 : 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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 0] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * 0) = 𝓝[I] (2 * 0)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
·

Goal state after:
case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)

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

Tactic:
·

Goal state after:
case e'_2
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

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

Tactic:
·

Goal state after:
case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)

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

Tactic:
·

Goal state after:
case e'_2
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

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

Tactic:
·

Goal state after:
case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case hf
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (fun x ↦ ω (γ.extend x)) (Icc 0 1)

pp: case hg
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (derivWithin ⇑γ.extend I) (Icc 0 1)

Tactic:
·

Goal state after:
case hf
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (fun x ↦ ω (γ.extend x)) (Icc 0 1)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case hg
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (derivWithin ⇑γ.extend I) (Icc 0 1)

Tactic:
·

Goal state after:
case hg
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (derivWithin ⇑γ.extend I) (Icc 0 1)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ‖∫ (y : ℝ) in a..b, deriv f y‖ ≤ ∫ (t : ℝ) in a..b, B t

pp: case hcont
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ContinuousOn f (uIcc a b)

pp: case hderiv
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x

pp: case hint
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
·

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ‖∫ (y : ℝ) in a..b, deriv f y‖ ≤ ∫ (t : ℝ) in a..b, B t
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hcont
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ContinuousOn f (uIcc a b)

pp: case hderiv
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x

pp: case hint
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
·

Goal state after:
case hcont
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ContinuousOn f (uIcc a b)