mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
⊢ ∃ x₀, μ = Measure.dirac x₀

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s = m (s ∩ ⋃ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m (s ∩ ⋃ i, f i) = m (⋃ i, s ∩ f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m (⋃ i, s ∩ f i) ≤ ∑' (i : ℕ), m (s ∩ f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ ∑' (i : ℕ), m (s ∩ f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
⊢ (OuterMeasure.ofFunction ⇑m ⋯) s = m s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
this : (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯) s = (AddContent.extend hC m) s
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯) s = m s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯) s = m s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ volume (closure s ∩ closedBall x (ε n)) / volume (closedBall x (ε n)) ≤
    volume (closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
i : ℕ
⊢ f i \ s = ⋃₀ ↑(A i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
⊢ (OuterMeasure.ofFunction ⇑m ⋯).IsCaratheodory s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).IsCaratheodory s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s✝ : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive
this : MeasurableSpace α := (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).caratheodory
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this✝ : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0
this : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet) (s ∆ t) < ENNReal.ofReal ε
⊢ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive
this : MeasurableSpace α := (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).caratheodory
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).trim ≤ inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this✝ : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0
this : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet) (s ∆ t) < ENNReal.ofReal ε
⊢ μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (m.measure hC ⋯ m_sigma_subadd) s = m s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
⊢ f = ∑ i, Pi.single i ∘ fun x ↦ f x i

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
this : f = ∑ i, Pi.single i ∘ fun x ↦ f x i
i : ι
x✝ : i ∈ Finset.univ
⊢ Pi.single i 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
⊢ MemLp f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable (fun x ↦ f x i) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
hf : ∀ (i : ι), Integrable (fun x ↦ f x i) μ
i : ι
⊢ (∫ (x : X), f x ∂μ) i = ∫ (x : X), f x i ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp f p μ
⊢ 0.1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp f p μ
⊢ 0.2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
⊢ f = (⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
this : f = (⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2
⊢ (AddMonoidHom.inl E F) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
this : f = (⇑(AddMonoidHom.inl E F) ∘ fun x ↦ (f x).1) + ⇑(AddMonoidHom.inr E F) ∘ fun x ↦ (f x).2
⊢ (AddMonoidHom.inr E F) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E × F
h : MemLp (fun x ↦ (f x).1) p μ ∧ MemLp (fun x ↦ (f x).2) p μ
⊢ MemLp f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
hμ : IsSeparable μ
⊢ IsSeparable μ.completion

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ WithLp.ofLp 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ MemLp f p μ ↔ ∀ (i : ι), MemLp (fun x ↦ (f x).ofLp i) p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ Integrable f μ ↔ ∀ (i : ι), Integrable (fun x ↦ (f x).ofLp i) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ q)
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
hf : ∀ (i : ι), Integrable (fun x ↦ (f x).ofLp i) μ
i : ι
⊢ (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ WithLp.ofLp 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (f x).fst) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ Integrable f μ ↔ Integrable (fun x ↦ (f x).fst) μ ∧ Integrable (fun x ↦ (f x).snd) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
x✝ : ℝ
d : ℕ
hyp : ∀ (b : ℕ), d ≤ b → x✝ ≤ ↑((μ (sub b)) (⋃ i, ⋃ (_ : i ≤ sub b), U i))
⊢ d ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
x✝ : ℝ
d : ℕ
hyp : ∀ (b : ℕ), d ≤ b → x✝ ≤ ↑((μ (sub b)) (⋃ i, ⋃ (_ : i ≤ sub b), U i))
⊢ ↑((μ (sub d)) (⋃ i, ⋃ (_ : i ≤ sub d), U i)) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).fst = ∫ (x : X), (f x).fst ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
f : (n : ℕ) × (Fin n → ↑u) × (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun nds ↦ key nds.fst nds.snd.1 nds.snd.2
this✝ : Countable ↑𝒜₀
this : Countable ↑u
⊢ D ⊆ range f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ liminf (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ n), U i))) atTop ≤
    liminf (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ sub k), U i))) atTop

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).snd = ∫ (x : X), (f x).snd ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
V : Type u_2
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
⊢ IsSigmaSubadditiveSetFun fun x ↦ ‖μ x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
V : Type u_2
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
⊢ ‖μ ∅‖ₑ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
⊢ 0 ≤ μ.real s ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
⊢ 0 < 3 * (1 + μ.real s ^ (1 / p.toReal))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
h : ∀ (δ : ℝ), 0 < δ → ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior sᶜ
⊢ ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
⊢ volume (frontier s) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
⊢ 0 < ε / 3

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
⊢ volume (frontier s) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ volume (frontier s) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ volume s = 0

Tactic:
by

Goal state after: