mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hh
a b : ℝ
⊢ Tendsto (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)

pp: case hgf
a b : ℝ
⊢ (fun x ↦ 0) ≤ fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

pp: case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

Tactic:
·

Goal state after:
case hh
a b : ℝ
⊢ Tendsto (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hgf
a b : ℝ
⊢ (fun x ↦ 0) ≤ fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

pp: case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

Tactic:
·

Goal state after:
case hgf
a b : ℝ
⊢ (fun x ↦ 0) ≤ fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

Tactic:
·

Goal state after:
case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))

Tactic:
·

Goal state after:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case left
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ 0 ≤ ∫ (x : ℝ) in a..b, deriv f x

pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
·

Goal state after:
case left
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ 0 ≤ ∫ (x : ℝ) in a..b, deriv f x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2)

pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2) + ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2) + ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2) + ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
    IntervalIntegrable f volume a b →
      a ≤ b → ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
hab : ¬a ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
    IntervalIntegrable f volume a b →
      a ≤ b → ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
hab : ¬a ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2)

pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2)

pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ 0 ≤ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case left
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ 0 ≤ ∫ (x : ℝ) in a..b, deriv f x

pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
· apply intervalIntegral.integral_nonneg_of_ae_restrict hab
    rw [Filter.EventuallyLE, ← restrict_Ioo_eq_restrict_Icc,
      MeasureTheory.ae_restrict_iff' measurableSet_Ioo]
    exact Filter.Eventually.of_forall @f_deriv_nonneg

Goal state after:
case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((fun x ↦ α • f x) (t.2 i).1) ((fun x ↦ α • f x) (t.2 i).2) ≤
    ‖α‖ * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
·

Goal state after:
case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
let g (x : ℝ) := if x ∈ Ioc a b then f x else 0

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : ℝ → E := fun x ↦ if x ∈ Ioc a b then f x else 0
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_3
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap ?convert_2 (totalLengthFilter ⊓ 𝓟 (disjWithin a b))

pp: case e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter) =
    comap ?convert_2 (comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0))

pp: case convert_2
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ ℝ × ℝ → ℕ × (ℕ → ℝ × ℝ)

Tactic:
·

Goal state after:
case e'_3
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap ?convert_2 (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter) =
    comap (fun x ↦ (1, fun x_1 ↦ x)) (comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0))

Tactic:
·

Goal state after:
case e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter) =
    comap (fun x ↦ (1, fun x_1 ↦ x)) (comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    0 ≤ ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2)

pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2) ≤
      C * ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2) +
        D * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
·

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    0 ≤ ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2)
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
hv : 0 ∈ ball 0 r
⊢ 0 ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

pp: case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
hv : 0 ∈ ball 0 r
⊢ 0 ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d η : ℝ
hη : 0 < η
hdb : d ≤ d
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d d → HasDerivAt f (f' x) x
⊢ ∃ u,
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < d) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint fun z ↦ Icc z.1 z.2) ∧ HasSum (fun z ↦ (↑z).2 - (↑z).1) (d - d)

pp: case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
⊢ ∃ u,
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint fun z ↦ Icc z.1 z.2) ∧ HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)

Tactic:
·

Goal state after:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d η : ℝ
hη : 0 < η
hdb : d ≤ d
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d d → HasDerivAt f (f' x) x
⊢ ∃ u,
    (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < d) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
      (u.PairwiseDisjoint fun z ↦ Icc z.1 z.2) ∧ HasSum (fun z ↦ (↑z).2 - (↑z).1) (d - d)