internlm/Lean-Github huggingface dataset:
Theorem: average_linear_comm
Proof state before:
case neg
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 → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
rw [(Ne.isUnit v0).inv.smul_left_cancel]
Proof state after:
case neg
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 → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ ∫ (x : X) in s, g (f x) = g (∫ (x : X) in s, f x)
Theorem: average_linear_comm
Proof state before:
case neg
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 → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ ∫ (x : X) in s, g (f x) = g (∫ (x : X) in s, f x)
Tactic:
exact ContinuousLinearMap.integral_comp_comm _ fi
Proof state after:
no goals
Theorem: average_congr_on
Proof 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 g : X → E
s : Set X
sn : NiceVolume s
h : ∀ᵐ (x : X), x ∈ s → f x = g x
⊢ ⨍ (x : X) in s, f x = ⨍ (x : X) in s, g x
Tactic:
simp only [← ae_restrict_iff' sn.measurable] at h
Proof 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 g : X → E
s : Set X
sn : NiceVolume s
h : ∀ᵐ (x : X) ∂volume.restrict s, f x = g x
⊢ ⨍ (x : X) in s, f x = ⨍ (x : X) in s, g x
Theorem: average_congr_on
Proof 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 g : X → E
s : Set X
sn : NiceVolume s
h : ∀ᵐ (x : X) ∂volume.restrict s, f x = g x
⊢ ⨍ (x : X) in s, f x = ⨍ (x : X) in s, g x
Tactic:
exact average_congr h
Proof state after:
no goals
Theorem: mean_bound
Proof 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]
Proof 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
Theorem: mean_bound
Proof 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
Proof 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
Theorem: mean_bound
Proof 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
Proof 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
Theorem: mean_bound
Proof 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 ⊢
Proof 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
Theorem: mean_bound
Proof 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)
Proof 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
Theorem: mean_bound
Proof 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
Proof 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
Theorem: mean_bound
Proof 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
Proof 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
Theorem: mean_bound
Proof 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]
Proof state after:
no goals
Theorem: mean_bound
Proof 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]
Proof state after:
no goals
Theorem: LocalVolume.closure_interior
Proof 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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
⊢ LocalVolumeSet s
Tactic:
intro x r xs rp
Proof 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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
⊢ 0 < ↑volume (s ∩ ball x r)
Theorem: LocalVolume.closure_interior
Proof 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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
have xci := ci xs
Proof 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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
⊢ 0 < ↑volume (s ∩ ball x r)
Theorem: LocalVolume.closure_interior
Proof 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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
rcases Metric.mem_closure_iff.mp xci r rp with ⟨y, ys, xy⟩
Proof state after:
case intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
⊢ 0 < ↑volume (s ∩ ball x r)
Theorem: LocalVolume.closure_interior
Proof state before:
case intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior y ys with ⟨e, ep, ye⟩
Proof state after:
case intro.intro.intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
⊢ 0 < ↑volume (s ∩ ball x r)
Theorem: LocalVolume.closure_interior
Proof state before:
case intro.intro.intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
set t := min e (r - dist x y)
Proof state after:
case intro.intro.intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ 0 < ↑volume (s ∩ ball x r)
Theorem: LocalVolume.closure_interior
Proof state before:
case intro.intro.intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
have es : ball y t ⊆ s ∩ ball x r := by
  simp only [Set.subset_inter_iff]; constructor
  exact _root_.trans (Metric.ball_subset_ball (by bound)) (_root_.trans ye interior_subset)
  apply Metric.ball_subset_ball'
  trans r - dist x y + dist y x; bound; simp [dist_comm]
Proof state after:
case intro.intro.intro.intro
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ 0 < ↑volume (s ∩ ball x r)