Theorem: mean_bound (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
⊢ ⨍ (x : X) in s, f x ≤ b
Tactic:
rw [average_eq, smul_eq_mul]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b
Tactic:
have bi := sn.integrableOn_const b
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b
Tactic:
have ib := setIntegral_mono_on fi bi sn.measurable fb
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b
Tactic:
simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, ge_iff_le] at ib ⊢
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ∫ (x : X) in s, f x ≤ b
Tactic:
trans (volume s).toReal⁻¹ * ((volume s).toReal * b)
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ∫ (x : X) in s, f x ≤ (↑volume s).toReal⁻¹ * ((↑volume s).toReal * b)

E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ((↑volume s).toReal * b) ≤ b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ∫ (x : X) in s, f x ≤ (↑volume s).toReal⁻¹ * ((↑volume s).toReal * b)
Tactic:
gcongr
State after:
case h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ ∫ (x : X) in s, f x ≤ (↑volume s).toReal * b

State before:
case h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ ∫ (x : X) in s, f x ≤ (↑volume s).toReal * b
Tactic:
apply le_trans ib
State after:
case h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ ∫ (x : X) in s, b ≤ (↑volume s).toReal * b

State before:
case h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ ∫ (x : X) in s, b ≤ (↑volume s).toReal * b
Tactic:
simp only [integral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  smul_eq_mul, le_refl]
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
fi : IntegrableOn f s volume
fb : ∀ z ∈ s, f z ≤ b
bi : IntegrableOn (fun x => b) s volume
ib : ∫ (x : X) in s, f x ≤ ∫ (x : X) in s, b
⊢ (↑volume s).toReal⁻¹ * ((↑volume s).toReal * b) ≤ b
Tactic:
rw [←mul_assoc _ _ b, inv_mul_cancel sn.real_nonneg, one_mul]
State after:
no goals