mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : 1 / 2 < t
ω✝ : E → E →L[𝕜] F
γab✝ : Path c b
γbc✝ : Path b a
⊢ 1 - t < 1 / 2

Tactic:
by

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

Goal state before:
pp: p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)

Tactic:
by

Goal state after:
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₀ : 1 / 2 < t
⊢ curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
by

Goal state after:
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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
⊢ 1 / 2 ≤ 1

Tactic:
by

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

Goal state before:
pp: α : 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 ρ
⊢ AEMeasurable ρ (μ.restrict s)

Tactic:
by

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

Goal state before:
pp: α : 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)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤

Tactic:
by

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

Goal state before:
pp: α : 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 < ⊤
⊢ (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, (ρ x).toReal * f x ∂μ

Tactic:
by

Goal state after:
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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
⊢ curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ι (1 / 2) 1)] fun t ↦ 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
by

Goal state after:
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
ω : E → E →L[𝕜] F
γab : Path a b
h : CurveIntegrable ω γab
γbc : Path b c
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume 0 (1 / 2)

Tactic:
by

Goal state after:
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
ω : E → E →L[𝕜] F
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ ∫ (x : α) in s, (ρ x).toReal * f x ∂μ = ∫ (x : α) in s, f x ∂ν

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν

Tactic:
by

Goal state after:
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
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
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
⊢ HasFDerivAt UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)

Tactic:
by

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

Goal state before:
pp: α : 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 ∂ν
h : (∫ (x : α) in s, 1 ∂μ.withDensity fun x ↦ ρ x) = ∫ (x : α) in s, (ρ x).toReal • 1 ∂μ
⊢ ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, (ρ x).toReal ∂μ

Tactic:
by

Goal state after:
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
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
⊢ ∫ᶜ (x : E) in γab.trans γbc, ω x = ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x

Tactic:
by

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

Goal state before:
pp: α : 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 ∂ν
h : (∫ (x : α) in s, 1 ∂μ.withDensity fun x ↦ ρ x) = ∫ (x : α) in s, (ρ x).toReal • 1 ∂μ
⊢ ∫ (x : α) in s, (ρ x).toReal ∂μ = ∫ (x : α) in s, 1 ∂ν

Tactic:
by

Goal state after:
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
inst✝ : NormedSpace ℝ E
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : t ∈ I
⊢ curveIntegralFun ω (Path.segment a b) t = (ω ((lineMap a b) t)) (b - a)

Tactic:
by

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

Goal state before:
pp: α : 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 ∂ν
⊢ ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
⊢ CurveIntegrable ω (Path.segment a b) ↔ IntervalIntegrable (fun t ↦ (ω ((lineMap a b) t)) (b - a)) volume 0 1

Tactic:
by

Goal state after:
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
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
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
⊢ deriv g t = ↑(deriv f t)

Tactic:
by

Goal state after:
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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
⊢ ∫ᶜ (x : E) in Path.segment a b, ω x = ∫ (t : ℝ) in 0..1, (ω ((lineMap a b) t)) (b - a)

Tactic:
by

Goal state after:
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
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace F
ω : E →L[𝕜] F
a b : E
⊢ ∫ᶜ (x : E) in Path.segment a b, ω = ω (b - a)

Tactic:
by

Goal state after:
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
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
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
hdg : ∀ t ∈ Ioo a b, deriv g t = ↑(deriv f t)
t : ℝ
htB : t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
ht : t ∈ Ioo a b
⊢ ‖deriv g t‖ ≤ B t

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x‖ ≤ C * ‖b - a‖ * |1 - 0|

Tactic:
let : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
    rw [curveIntegral_segment]
    refine intervalIntegral.norm_integral_le_of_norm_le_const fun t ht ↦ ?_
    rw [segment_eq_image_lineMap] at h
    rw [uIoc_of_le zero_le_one] at ht
    apply_rules [(ω _).le_of_opNorm_le, mem_image_of_mem, Ioc_subset_Icc_self]

Goal state after:
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 : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x‖ ≤ C * ‖b - a‖ * |1 - 0|

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
⊢ C * ‖b - a‖ * |1 - 0| = C * ‖b - a‖

Tactic:
by

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

Goal state before:
pp: α : 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 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ (fun x ↦ f x * g x) =ᵐ[μ.restrict s] 0

Tactic:
by

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

Goal state before:
pp: α : 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 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x * g x ∂μ = 0

Tactic:
by

Goal state after:
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 : 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 (⇑γ.extend) (Icc 0 1)

Tactic:
by

Goal state after:
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
⊢ (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B

Tactic:
by

Goal state after:
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 : 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
⊢ CurveIntegrable ω γ

Tactic:
by

Goal state after:
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 : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ

Tactic:
by

Goal state after:
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 : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ CurveIntegrable (ω₁ + ω₂) γ

Tactic:
by

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

Goal state before:
pp: α : 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 : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x ∂ν = 0

Tactic:
by

Goal state after:
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 : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x

Tactic:
by

Goal state after:
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 : E
γ : Path a b
⊢ curveIntegralFun 0 γ = 0

Tactic:
by

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

Goal state before:
pp: α : 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 : α
hc : c ∈ s
⊢ 0 = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
by

Goal state after:
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 : E
γ : Path a b
⊢ CurveIntegrable 0 γ

Tactic:
by

Goal state after:
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 : E
γ : Path a b
⊢ curveIntegral 0 γ = 0

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (-ω) γ = -curveIntegralFun ω γ

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable ω γ
⊢ CurveIntegrable (-ω) γ

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable (-ω) γ
⊢ CurveIntegrable ω γ

Tactic:
by

Goal state after:
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegral (-ω) γ = -∫ᶜ (x : E) in γ, ω x

Tactic:
by

Goal state after:
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 : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ

Tactic:
by

Goal state after: