E : Type u_1
X : Type ?u.1741316
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (Function.support fun i => ↑f i)
E : Type u_1
X : Type ?u.1741316
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ 0 < ∫ (x : E), ↑f x ∂μ
refine' (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr _
E : Type u_1
X : Type ?u.1741316
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (ball c f.rOut)
E : Type u_1
X : Type ?u.1741316
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (Function.support fun i => ↑f i)
rw [f.support_eq]
no goals
E : Type u_1
X : Type ?u.1741316
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (ball c f.rOut)
exact measure_ball_pos μ c f.rOut_pos