mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
s t : Set X
h : AreSeparated s t
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t : Set X
h : AreSeparated s t
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x)) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ

Tactic:
simpa using

Goal state after:
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ (r - x)⁻¹) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ

Tactic:
simpa using

Goal state after:
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ ((r - x) ^ 2)⁻¹)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: ⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) 0 1

Tactic:
simpa using

Goal state after:
⊢ HasFPowerSeriesOnBall (fun x ↦ ((1 - x) ^ 2)⁻¹) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) 0 1
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : Set X
t : ι → Set X
⊢ AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : Set X
t : ι → Set X
⊢ AreSeparated (⋃ i ∈ I, t i) s ↔ ∀ i ∈ I, AreSeparated (t i) s
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε s C
⊢ IsCover ε (f '' s) (f '' C)

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε s C
⊢ IsCover ε (f '' s) (f '' C)
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s N : Set X
hN : Maximal (fun N ↦ N ⊆ s ∧ IsSeparated (↑ε) N) N
⊢ Maximal (fun N ↦ N ⊆ s ∧ SetRel.IsSeparated {(x, y) | edist x y ≤ ↑ε} N) N

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s N : Set X
hN : Maximal (fun N ↦ N ⊆ s ∧ IsSeparated (↑ε) N) N
⊢ Maximal (fun N ↦ N ⊆ s ∧ SetRel.IsSeparated {x | edist x.1 x.2 ≤ ↑ε} N) N
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst✝ : ProperSpace X
hN : IsClosed N
⊢ IsCover ε (closure s) N ↔ IsCover ε s N

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst✝ : ProperSpace X
hN : IsClosed N
⊢ closure s ⊆ cthickening (↑ε) N ↔ s ⊆ cthickening (↑ε) N
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < packingRadius

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < D.packingRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsSeparated (↑packingRadius) carrier

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsSeparated (↑D.packingRadius) D.carrier
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < coveringRadius

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ 0 < D.coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsCover coveringRadius Set.univ carrier

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
D : DeloneSet X
carrier : Set X
packingRadius coveringRadius : ℝ≥0
h_carrier : carrier = D.carrier
h_packing : packingRadius = D.packingRadius
h_covering : coveringRadius = D.coveringRadius
⊢ IsCover D.coveringRadius Set.univ D.carrier
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ENNReal.ofReal ↑D.packingRadius < ENNReal.ofReal (dist x y)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ ↑D.packingRadius < dist x y
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist : (x, y) ∈ {(x, y) | edist x y ≤ ↑D.coveringRadius}
⊢ dist x y ≤ ↑D.coveringRadius

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist : (x, y) ∈ {(x, y) | edist x y ≤ ↑D.coveringRadius}
⊢ nndist x y ≤ D.coveringRadius
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
rw [linearGrowthSup, limsup_le_iff']

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / ↑a ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * 0 a) l (𝓝 0)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a ↦ 0) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (f + g) a) l (𝓝 0)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * f a + k a ^ z * g a) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (fun n ↦ f n * c) a) l (𝓝 0)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * f a * c) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen[inst✝¹] s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a ↦ k a ^ (z + 1) * f a) ⁻¹' s
⊢ x ∈ (fun a ↦ k a ^ z * (k * f) a) ⁻¹' s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen[inst✝¹] s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a ↦ k a ^ (z + 1) * f a) ⁻¹' s
⊢ k x ^ (z + 1) * f x ∈ s
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ 0 * f)

Tactic:
simpa using

Goal state after:
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k f
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f)

Tactic:
simpa using

Goal state after:
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k * (k ^ n * f))
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n ↦ f n * c
x : α
⊢ f x * c * c⁻¹ = f x

Tactic:
by simp [mul_assoc, mul_inv_cancel₀ hc0]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f) ↔ SuperpolynomialDecay l k f

Tactic:
simpa using

Goal state after:
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ m / τ ≤ δ a

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ 0 ≤ δ a
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
have he₂ : ∀ n, γ - (1 / 2) ^ n < d (e n) := fun n => (he n).2

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
hfi : Integrable f μ
⊢ ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
hfi : Integrable f μ
⊢ ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hf : IntegrableOn f s μ
hf₀ : 0 ≤ᵐ[μ.restrict s] f
⊢ ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hf : IntegrableOn f s μ
hf₀ : 0 ≤ᵐ[μ.restrict s] f
⊢ ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ (∫⁻ (x : α) in s, f x ∂μ).toReal / (μ s).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : IntegrableOn f s μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : IntegrableOn f s μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, f x ≤ ∫ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, ∫ (a : α), f a ∂μ ≤ f x
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa using

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x