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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p = ∞
h : MemLp μ[f | m] ∞ μ
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
simp_all only [lpNorm_exponent_top_eq_essSup]
          exact hf.essSup_norm_condExp_le_essSup_norm

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))

Tactic:
convert! tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case funProp.discharger
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp✝ : 1 ≤ p
hf : MemLp f p μ
hp' : 0 < p
hpt : p ≠ ∞
hp : 1 ≤ p.toReal
this : (fun x ↦ ‖μ[f | m] x‖ ^ p.toReal) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p.toReal | m]
⊢ 0 ≤ p.toReal

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑⟨Measure.map f ↑(νs x✝), ⋯⟩ = ∫⁻ (ω : Ω), ↑(g (f ω)) ∂↑(νs x✝)

Tactic:
refine lintegral_map ?_ f_cont.measurable

Goal state after:
case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ Measurable fun ω ↦ ↑(g ω)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑⟨Measure.map f ↑ν, ⋯⟩ = ∫⁻ (ω : Ω), ↑(g (f ω)) ∂↑ν

Tactic:
refine lintegral_map ?_ f_cont.measurable

Goal state after:
case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ Measurable fun ω ↦ ↑(g ω)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
⊢ UniformIntegrable (fun i ↦ μ[g | ℱ i]) 1 μ

Tactic:
let A : MeasurableSpace α := m0

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
⊢ UniformIntegrable (fun i ↦ μ[g | ℱ i]) 1 μ
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
hT : IsTightMeasureSet T
hST : S ⊆ T
x✝ : Set 𝓧
⊢ 0 ≤ (⨆ μ ∈ S, ⇑μ) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_5
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ 0 = max 0 0

Tactic:
simp

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

Goal state before:
pp: case inr
Ω : 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 : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
⊢ μ Eᶜ ≤ liminf (fun i ↦ (μs i) Eᶜ) L

Tactic:
have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne

Goal state after:
case inr
Ω : 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 : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
⊢ μ Eᶜ ≤ liminf (fun i ↦ (μs i) Eᶜ) L
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : 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
hne : L.NeBot
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ

Tactic:
have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne

Goal state after:
case inr
Ω : 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
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ 𝕜), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
f : Ω →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))

Tactic:
specialize h ((RCLike.ofRealAm (K := 𝕜)).compLeftContinuousBounded ℝ
      RCLike.lipschitzWith_ofReal f)
    simp only [AlgHom.compLeftContinuousBounded_apply_apply, RCLike.ofRealAm_coe,
      integral_ofReal] at h
    exact tendsto_ofReal_iff'.mp h

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

Goal state before:
pp: case e'_3
Ω : 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))
B : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑i.2) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑p.2))
q : FiniteMeasure Ω × FiniteMeasure Ω
⊢ ∫⁻ (x : Ω), ↑(g x) ∂↑(q.1 + q.2) = ∫⁻ (x : Ω), ↑(g x) ∂↑q.1 + ∫⁻ (x : Ω), ↑(g x) ∂↑q.2

Tactic:
simp

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

Goal state before:
pp: case e'_5
Ω : 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))
B : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑i.2) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑p.2))
⊢ ∫⁻ (x : Ω), ↑(g x) ∂↑((fun p ↦ p.1 + p.2) p) = ∫⁻ (x : Ω), ↑(g x) ∂↑p.1 + ∫⁻ (x : Ω), ↑(g x) ∂↑p.2

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
peel 3

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
⊢ (∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)) ↔
    ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_2.inl
α : 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 ε
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑0)⁻¹ • f i) = (↑0)⁻¹ • s.indicator (f i)
⊢ ∑ i ∈ Finset.range 0, eLpNorm (s.indicator ((↑0)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : 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 : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑⟨Measure.map f ↑(νs x✝), ⋯⟩ = ∫⁻ (x : Ω), ↑(g (f x)) ∂↑(νs x✝)

Tactic:
refine lintegral_map ?_ f_cont.measurable

Goal state after:
case e'_3
Ω : 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 : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ Measurable fun x ↦ ↑(g x)
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:
simp

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

Goal state before:
pp: case e'_5
Ω : 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 : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑⟨Measure.map f ↑ν, ⋯⟩ = ∫⁻ (x : Ω), ↑(g (f x)) ∂↑ν

Tactic:
refine lintegral_map ?_ f_cont.measurable

Goal state after:
case e'_5
Ω : 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 : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ Measurable fun x ↦ ↑(g x)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3.inl
α : 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 μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
⊢ ∑ i ∈ Finset.range 0, eLpNorm ((↑0)⁻¹ • f i) p μ ≤ ↑C

Tactic:
simp

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
    simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton

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

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
f : ι → Set Ω
hf : ∀ i ∈ ∅, f i ∈ m i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ ∅, f i) = ∏ i ∈ ∅, (κ a) (f i)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
f : ι → Set Ω
i : ι
hf : ∀ i_1 ∈ {i}, f i_1 ∈ m i_1
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i_1 ∈ {i}, f i_1) = ∏ i ∈ {i}, (κ a) (f i)

Tactic:
simp

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 Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
⊢ (∀ i ∈ s, f i ∈ (π ∘ g) i) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
hf

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
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 Ω
⊢ ↑μ (f ⁻¹' (range f)ᶜ) = 0

Tactic:
simp

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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) ⊥ (𝓝 (μ E))
⊢ limsup (fun i ↦ (μs i) F) ⊥ ≤ μ F

pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F

Tactic:
· simp only [limsup_bot, bot_eq_zero', zero_le]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
inst✝ : IsZeroOrMarkovKernel 0
⊢ ∀ᵐ (a : α) ∂μ, (0 a) (s ∩ t) = (0 a) s * (0 a) t

Tactic:
simp

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

Goal state before:
pp: case hs
Ω' : 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
μ : ↑M
s : Set Ω'
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
· exact hf.continuous.measurable hs

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

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
μ : Measure α
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
ht2m : MeasurableSet t2
inst✝ : IsZeroOrMarkovKernel 0
hyp : IndepSets p1 p2 0 μ
⊢ ∀ᵐ (a : α) ∂μ, (0 a) (t1 ∩ t2) = (0 a) t1 * (0 a) t2

Tactic:
simp

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

Goal state before:
pp: case inr.empty
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ∅) = (κ a) t1 * (κ a) ∅

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
⊢ ∀ (x : ℝ≥0∞), (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
μ : Measure α
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
inst✝ : IsZeroOrMarkovKernel 0
hyp : IndepSets p1 p2 0 μ
⊢ Indep m1 m2 0 μ

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ (μs x) G) atTop, (fun x1 x2 ↦ x1 ≤ x2) x 1

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f✝ : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (s.restrict f✝) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
x✝ : Ω
⊢ x✝ ∈ ⋂ i ∈ s, f i ↔ x✝ ∈ ⋂ i, f ↑i

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ (μs x) G) atTop, (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case right.e_6
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : Ω
⊢ x ∈ ⋂ i, f i ⁻¹' s i ↔ x ∈ (fun c x ↦ f x c) ⁻¹' univ.pi s

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst✝²] G
⊢ ∀ (x : ι), (μs x) G ≤ 1

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
h : limsup (fun i ↦ (μs i) F) atTop ≤ μ F
hF_closed : IsClosed[inst✝¹] F
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ (μs x) F) atTop, (fun x1 x2 ↦ x1 ≤ x2) x 1

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
h : limsup (fun i ↦ (μs i) F) atTop ≤ μ F
hF_closed : IsClosed[inst✝¹] F
⊢ ∀ (a : ℝ≥0), (∀ᶠ (x : ℝ≥0) in map (fun x ↦ (μs x) F) atTop, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) 0 a

Tactic:
simp

Goal state after: