Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rcases le_total a b with hab | hab
State after:
case inl
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case inr
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

State before:
case inl
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [intervalIntegral.integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
← integral_indicator measurableSet_Icc, indicator_eq_self.2 h]
State after:
no goals

State before:
case inr
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
by_cases hab2 : b = a
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [hab2] at h ⊢
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..a, f x ∂μ = ∫ (x : ℝ), f x ∂μ

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..a, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
simp only [intervalIntegral.integral_same]
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ 0 = ∫ (x : ℝ), f x ∂μ

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
simp only [Icc_self] at h
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ 0 = ∫ (x : ℝ), f x ∂μ

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by
  rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = ∫ (x : ℝ), f x ∂μ

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [this, integral_singleton]
State after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = (μ {a}).toReal • f a

State before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = (μ {a}).toReal • f a
Tactic:
simp
State after:
no goals

State before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
Tactic:
rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ MeasurableSet {a}
Tactic:
simp
State after:
no goals

State before:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [Icc_eq_empty_iff.mpr <| by exact fun x ↦ hab2 <| le_antisymm hab x, subset_empty_iff,
    Function.support_eq_empty_iff] at h
State after:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : f = 0
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

State before:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : f = 0
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
simp [h]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ¬a ≤ b
Tactic:
exact fun x ↦ hab2 <| le_antisymm hab x
State after:
no goals