mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h : IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) (AEMeasurable.mk (f k) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f k) ⋯ =ᵐ[κ a] f k

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h : IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) (AEMeasurable.mk (f k) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f k) ⋯ =ᵐ[κ a] f k
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ ∀ᵐ (a : α) ∂μ, (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)

pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ ∀ᵐ (a : α) ∂μ, (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) =ᵐ[κ a] fun a ↦ (f k a, f l a)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ ∀ᵐ (a : α) ∂μ, (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ ∀ᵐ (a : α) ∂μ, (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) =ᵐ[κ a] fun a ↦ (f k a, f l a)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
⊢ ∀ᵐ (a : α) ∂μ, (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) =ᵐ[κ a] fun a ↦ (f k a, f l a)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, ∏ j ∈ s, AEMeasurable.mk (f j) ⋯ =ᵐ[κ a] ∏ j ∈ s, f j

pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᵐ[κ a] f i

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, ∏ j ∈ s, AEMeasurable.mk (f j) ⋯ =ᵐ[κ a] ∏ j ∈ s, f j
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᵐ[κ a] f i

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᵐ[κ a] f i
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h₁.refine_2
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ∀ x ∈ {x | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n x) - F (X n x)‖ ≤ ↑L * (ε / 2)

Tactic:
·

Goal state after:
case h₁.refine_2
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ∀ x ∈ {x | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n x) - F (X n x)‖ ≤ ↑L * (ε / 2)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 1 ∉ π i
⊢ MeasurableSet ∅

pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 0 ∉ π i
⊢ MeasurableSet ∅

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 1 ∉ π i
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 0 ∉ π i
⊢ MeasurableSet ∅

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 0 ∉ π i
⊢ MeasurableSet ∅
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h₂
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'' ≤
    ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ''

Tactic:
·

Goal state after:
case h₂
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'' ≤
    ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ''
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ sInf ((fun f ↦ ↑f i) '' x✝), mono' := ⋯, le' := ⋯ }

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : ¬x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ m, mono' := ⋯, le' := ⋯ }

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ sInf ((fun f ↦ ↑f i) '' x✝), mono' := ⋯, le' := ⋯ }
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : ¬x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ m, mono' := ⋯, le' := ⋯ }

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : ¬x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ m, mono' := ⋯, le' := ⋯ }
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ 0 < ↑‖1 x‖₊

pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ (⋂ n ∈ u, s n).indicator 1 =ᵐ[μ] 0

Tactic:
·

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ 0 < ↑‖1 x‖₊
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕 j

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ (⋂ n ∈ u, s n).indicator 1 =ᵐ[μ] 0

Tactic:
·

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ (⋂ n ∈ u, s n).indicator 1 =ᵐ[μ] 0
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : (𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕 j

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

pp: case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)

Tactic:
·

Goal state after:
case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
j : ι
hj : ¬(𝓝[>] j).NeBot
hij : j ≤ j
hi : (𝓝[>] j).NeBot
⊢ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1 ≤ ↑𝓕 j

pp: case neg.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj✝ : ¬(𝓝[>] j).NeBot
hj : j ≠ i
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j

Tactic:
·

Goal state after:
case neg.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
j : ι
hj : ¬(𝓝[>] j).NeBot
hij : j ≤ j
hi : (𝓝[>] j).NeBot
⊢ ⨅ j_1, ⨅ (_ : j < j_1), ↑𝓕 j_1 ≤ ↑𝓕 j