-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem integral_le_measure_closedBall : ∫ x, f x ∂μ ≤ (μ (closedBall c f.rOut)).toReal

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ f.rOut < dist x c

Tactic:
simpa using hx

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntegrableOn (fun x => 1) (closedBall c f.rOut) μ

Tactic:
simp [measure_closedBall_lt_top]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ ≤ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ

Tactic:
apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntegrableOn (fun x => 1) (closedBall c f.rOut) μ

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ = ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ

Tactic:
apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ ↑f x = 0

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ ↑f x = 0

Tactic:
apply f.zero_of_le_dist (le_of_lt _)

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ f.rOut < dist x c

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = (μ (closedBall c f.rOut)).toReal

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ ≤ (μ (closedBall c f.rOut)).toReal

Tactic:
calc
∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
apply f.zero_of_le_dist (le_of_lt _)
simpa using hx
_ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
simp [measure_closedBall_lt_top]
_ = (μ (closedBall c f.rOut)).toReal := by simp

Result:
no goals