[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
x : E
⊢ ContDiffBump.normed f μ (c - x) = ContDiffBump.normed f μ (c + x)
[PROOFSTEP]
simp_rw [f.normed_def, f.sub]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
c : E
f✝ : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
f : ContDiffBump 0
x : E
⊢ ContDiffBump.normed f μ (-x) = ContDiffBump.normed f μ x
[PROOFSTEP]
simp_rw [f.normed_def, f.neg]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
refine' (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr _
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (support fun i => ↑f i)
[PROOFSTEP]
rw [f.support_eq]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (ball c f.rOut)
[PROOFSTEP]
exact measure_ball_pos μ c f.rOut_pos
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ContDiffBump.normed f μ x ∂μ = 1
[PROOFSTEP]
simp_rw [ContDiffBump.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul, integral_smul]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ (∫ (x : E), ↑f x ∂μ)⁻¹ • ∫ (x : E), ↑f x ∂μ = 1
[PROOFSTEP]
exact inv_mul_cancel f.integral_pos.ne'
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ support (ContDiffBump.normed f μ) = ball c f.rOut
[PROOFSTEP]
unfold ContDiffBump.normed
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ (support fun x => ↑f x / ∫ (x : E), ↑f x ∂μ) = ball c f.rOut
[PROOFSTEP]
rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ tsupport (ContDiffBump.normed f μ) = closedBall c f.rOut
[PROOFSTEP]
rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ HasCompactSupport (ContDiffBump.normed f μ)
[PROOFSTEP]
simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
⊢ Tendsto (fun i => support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
[PROOFSTEP]
simp_rw [NormedAddCommGroup.tendsto_nhds_zero, Real.norm_eq_abs, abs_eq_self.mpr (φ _).rOut_pos.le] at hφ 
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ Tendsto (fun i => support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
[PROOFSTEP]
rw [nhds_basis_ball.smallSets.tendsto_right_iff]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support fun x_1 => ContDiffBump.normed (φ x) μ x_1) ∈ 𝒫 ball c i
[PROOFSTEP]
refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (support fun x => ContDiffBump.normed (φ i) μ x) ∈ 𝒫 ball c ε
[PROOFSTEP]
rw [(φ i).support_normed_eq]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε
[PROOFSTEP]
exact ball_subset_ball hi.le
[GOAL]
E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : HasContDiffBump E
inst✝⁷ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁶ : BorelSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : IsLocallyFiniteMeasure μ
inst✝³ : IsOpenPosMeasure μ
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : CompleteSpace X
z : X
⊢ ∫ (x : E), ContDiffBump.normed f μ x • z ∂μ = z
[PROOFSTEP]
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
calc
  (μ (closedBall c f.rIn)).toReal = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
  _ = ∫ x in closedBall c f.rIn, f x ∂μ :=
    (set_integral_congr (measurableSet_closedBall) (fun x hx ↦ (one_of_mem_closedBall f hx).symm))
  _ ≤ ∫ x, f x ∂μ := set_integral_le_integral f.integrable (eventually_of_forall (fun x ↦ f.nonneg))
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ContDiffBump.normed f μ x ≤ 1 / ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
rw [normed_def]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ↑f x / ∫ (x : E), ↑f x ∂μ ≤ 1 / ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
gcongr
[GOAL]
case hd
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ 0 < ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne
[GOAL]
case hac
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ↑f x ≤ 1
[PROOFSTEP]
exact f.le_one
[GOAL]
case hbd
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
exact f.measure_closedBall_le_integral μ
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ ≤ ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ :=
    by
    apply (set_integral_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 set_integral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = (μ (closedBall c f.rOut)).toReal := by simp
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ = ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ
[PROOFSTEP]
apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
hx : ¬x ∈ closedBall c f.rOut
⊢ ↑f x = 0
[PROOFSTEP]
apply f.zero_of_le_dist (le_of_lt _)
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
hx : ¬x ∈ closedBall c f.rOut
⊢ f.rOut < dist x c
[PROOFSTEP]
simpa using hx
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ ≤ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ
[PROOFSTEP]
apply set_integral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ IntegrableOn (fun x => 1) (closedBall c f.rOut)
[PROOFSTEP]
simp [measure_closedBall_lt_top]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
have K_pos : 0 < K := by simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ 0 < K
[PROOFSTEP]
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
apply le_trans _ (f.measure_closedBall_le_integral μ)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
rw [div_le_iff (pow_pos K_pos _), addHaar_closedBall' _ _ f.rIn_pos.le, addHaar_closedBall' _ _ f.rOut_pos.le,
  ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (pow_nonneg f.rOut_pos.le _),
  ENNReal.toReal_ofReal (pow_nonneg f.rIn_pos.le _), mul_assoc, mul_comm _ (K ^ _), ← mul_assoc, ← mul_pow,
  mul_comm _ K]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ f.rOut ^ finrank ℝ E * ENNReal.toReal (↑↑μ (closedBall 0 1)) ≤
    (K * f.rIn) ^ finrank ℝ E * ENNReal.toReal (↑↑μ (closedBall 0 1))
[PROOFSTEP]
gcongr
[GOAL]
case h.ha
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut
[PROOFSTEP]
exact f.rOut_pos.le
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
have K_pos : 0 < K := by simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ 0 < K
[PROOFSTEP]
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
  gcongr
  · exact f.integral_pos.le
  · exact f.le_one
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
[PROOFSTEP]
gcongr
[GOAL]
case hc
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ 0 ≤ ∫ (y : E), ↑f y ∂μ
[PROOFSTEP]
exact f.integral_pos.le
[GOAL]
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ↑f x ≤ 1
[PROOFSTEP]
exact f.le_one
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
apply this.trans
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ 1 / ∫ (y : E), ↑f y ∂μ ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
rw [div_le_div_iff f.integral_pos, one_mul, ← div_le_iff' (pow_pos K_pos _)]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
exact f.measure_closedBall_div_le_integral μ K h
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ 0 < ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne' measure_closedBall_lt_top.ne
