mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal) ≤ eLpNorm ({x | C ≤ ‖f (ℐ C) x‖₊}.indicator (f (ℐ C))) p μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑i.1) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑p.1))

Tactic:
by

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
⊢ ∀ (C : ℝ≥0), C • ↑δ ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ

Tactic:
by

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
⊢ 0 < ε / 2

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑i.1) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑p.1))
⊢ Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑i.2) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑p.2))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ ContinuousAdd (FiniteMeasure Ω)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ

Tactic:
by

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hK₁_le : (Measure.map Prod.fst κ) K₁ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ AEMeasurable Prod.fst κ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
⊢ Tendsto (fun i ↦ i.1) (𝓝 p) (𝓝 p.1)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun i ↦ i.1) (𝓝 p) (𝓝 p.1)
⊢ Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑i.2) (𝓝 p) (𝓝 (∫ (x : Ω), g x ∂↑p.2))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), μ {x | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ

Tactic:
by

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
κ : Measure (𝓧 × 𝓨)
hK₂_le : (Measure.map Prod.snd κ) K₂ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ AEMeasurable Prod.snd κ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ ContinuousSMul ℝ≥0 (FiniteMeasure Ω)

Tactic:
by

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : IsTightMeasureSet (Measure.fst '' μ)
hμ₂ : IsTightMeasureSet (Measure.snd '' μ)
⊢ IsTightMeasureSet μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → FiniteMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Continuous[inst✝, _] fun x ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed[inst✝³] F → limsup (fun i ↦ (μs i) F) L ≤ μ F) ↔
    ∀ (G : Set Ω), IsOpen[inst✝³] G → μ G ≤ liminf (fun i ↦ (μs i) G) L

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
π : ι → Set (Set Ω)
⊢ iIndepSets π κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s1 s2 : Set (Set Ω)
⊢ IndepSets s1 s2 κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s1 s2 : Set (Set Ω)
⊢ IndepSets s1 s2 0 μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ iIndep m κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ Indep m₁ m₂ κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
μ : Measure α
m₁ m₂ _mΩ : MeasurableSpace Ω
⊢ Indep m₁ m₂ 0 μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s : ι → Set Ω
⊢ iIndepSet s κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s t : Set Ω
⊢ IndepSet s t κ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
⊢ IndepSet s t 0 μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → FiniteMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔ ∀ (f : Ω →ᵇ ℝ), Continuous[inst✝, _] fun x ↦ ∫ (ω : Ω), f ω ∂↑(μs x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ IsFiniteMeasure (Measure.comap f ↑μ)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ (comap f μ).mass ≤ μ.mass

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
x : Ω
⊢ g x = g' (f x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i ↦ (μs i) E₀) L
h_E₁ : limsup (fun i ↦ (μs i) E₁) L ≤ μ E₁
⊢ Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
ν : FiniteMeasure Ω'
hν : ν (range f)ᶜ = 0
⊢ ∫ (y : Ω') in range f, g' y ∂↑ν = ∫ (y : Ω'), g' y ∂↑ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
B : ∀ {ν : FiniteMeasure Ω'}, ν (range f)ᶜ = 0 → ∫ (y : Ω') in range f, g' y ∂↑ν = ∫ (y : Ω'), g' y ∂↑ν
⊢ Tendsto (fun ν ↦ ∫ (y : Ω'), g' y ∂↑ν) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (y : Ω'), g' y ∂↑μ))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
⊢ iIndepSets π κ μ ↔ iIndepSets π η μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
⊢ ContinuousOn (fun μ ↦ comap f μ) {μ | μ (range f)ᶜ = 0}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
⊢ (ν.map f) A = ν (f ⁻¹' A)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
⊢ (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
⊢ (c • ν).map f = c • ν.map f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
⊢ (μ.map f).mass ≤ μ.mass

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
⊢ IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ i ∈ ∅, univ ∈ π i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ (κ a) univ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
⊢ limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
⊢ limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ ↑μ (frontier ?m.34) = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
hE : IsClopen E
⊢ μ (frontier E) = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Function.onFun Disjoint fun r ↦ frontier (Metric.thickening r s))
key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable
aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)
⊢ 0 < ENNReal.ofReal (b - a)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
⊢ s = ∅ ∨ ∃ i, s = {i}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ iIndepSets m κ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → MeasurableSpace Ω
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ iIndep m κ μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : Tendsto νs L (𝓝 ν)
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ Tendsto (fun i ↦ (νs i).map f) L (𝓝 (ν.map f))

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun ν ↦ ν.map f

Tactic:
by

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

Goal state before:
pp: Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
⊢ ↑M

Tactic:
by

Goal state after: