awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h'c : μ {ω | c ≤ ‖f ω‖₊} < ∞ := hℒp.meas_ge_lt_top hp hp' c_pos.ne'
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊}) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' Set.univ) : ℝ≥0∞)

Tactic:
have := hindep.measure_inter_preimage_eq_mul {x | c ≤ ‖x‖₊} Set.univ
    (isClosed_le continuous_const continuous_nnnorm).measurableSet MeasurableSet.univ
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊}) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' Set.univ) : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp only [Set.preimage_setOf_eq, Set.preimage_univ, Set.inter_univ] at this

Premises used: Set.inter_univ, Set.preimage_setOf_eq, Set.preimage_univ
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ IsProbabilityMeasure μ

Tactic:
⟨(ENNReal.mul_eq_left hc.ne' h'c.ne).1 this.symm⟩

Premises used: LT.lt.ne', ENNReal.mul_eq_left, Iff.mp, MeasureTheory.IsProbabilityMeasure.mk, Eq.symm, LT.lt.ne
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ IsProbabilityMeasure μ

Tactic:
exact ⟨(ENNReal.mul_eq_left hc.ne' h'c.ne).1 this.symm⟩
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
hf : Integrable f μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
⊢ IsProbabilityMeasure μ

Tactic:
MemLp.isProbabilityMeasure_of_indepFun f g one_ne_zero ENNReal.one_ne_top
    (memLp_one_iff_integrable.mpr hf) h'f hindep

Premises used: Iff.mpr, MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun, one_ne_zero, MeasureTheory.memLp_one_iff_integrable, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
⊢ Eq.{u_3 + 1} (α := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)
    (Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) : Measure γ)

Tactic:
rfl

Premises used: MeasureTheory.Measure.join, MeasureTheory.Measure.bind, MeasureTheory.Measure.ofMeasurable, rfl
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
rw :
  ((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
rw₁ rw₂ :
  ∫⁻ (a : β), (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a

Tactic:
rw [comp_apply, Measure.bind_apply hs (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, ProbabilityTheory.Kernel.comp_apply
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
rw :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
rw [comp_apply' _ _ _ .univ]

Premises used: ProbabilityTheory.Kernel.comp_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (x : β), Cη ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_mono fun b => measure_le_bound η b Set.univ

Premises used: Set.univ, MeasureTheory.lintegral_mono, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (x : β), Cη ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (β := ℝ≥0∞) Cη ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
MeasureTheory.lintegral_const Cη

Premises used: MeasureTheory.lintegral_const
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
Cη : ℝ≥0∞ := η.bound
⊢ HMul.hMul (β := ℝ≥0∞) Cη ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) Cη

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
calc
    ∫⁻ b, η b Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a :=
      lintegral_mono fun b => measure_le_bound η b Set.univ
    _ = Cη * κ a Set.univ := MeasureTheory.lintegral_const Cη
    _ = κ a Set.univ * Cη := mul_comm _ _

Premises used: MeasureTheory.lintegral_const, Set.univ, MeasureTheory.lintegral_mono, ProbabilityTheory.Kernel.measure_le_bound, mul_comm, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
h :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((0 ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α γ) (0 ∘ₖ κ) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
a : α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((0 ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [comp_apply]

Premises used: ProbabilityTheory.Kernel.comp_apply
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
h :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ ∘ₖ 0 : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α γ) (κ ∘ₖ 0) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a : α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ 0 : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [comp_apply]

Premises used: ProbabilityTheory.Kernel.comp_apply
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((Kernel.id ∘ₖ κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Kernel.id ∘ₖ κ = κ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((Kernel.id ∘ₖ κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [comp_apply' _ _ _ hs, id_apply, Measure.dirac_apply' _ hs]
    using lintegral_indicator_one hs

Premises used: MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.id_apply, MeasureTheory.lintegral_indicator_one, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
h :
  ∀ (a : β) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ ∘ₖ Kernel.id : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ ∘ₖ Kernel.id = κ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a : β
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ Kernel.id : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [comp_apply' _ _ _ hs, id_apply,
    lintegral_dirac' a <| κ.measurable_coe hs]

Premises used: MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_

Premises used: MeasureTheory.measurableSet_toMeasurable, ProbabilityTheory.Kernel.measurable_coe, MeasureTheory.ae_lt_top
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∫⁻ (x : β),
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) ∂(κ : (a : α) → Measure β) a ≠
    ∞
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_

Premises used: MeasureTheory.measurableSet_toMeasurable, ProbabilityTheory.Kernel.measurable_coe, MeasureTheory.ae_lt_top
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa :
  Ne (α := ℝ≥0∞)
    ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ :
  Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : β),
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) ∂(κ : (a : α) → Measure β) a ≠
    ∞

Tactic:
rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
have h : ∀ᵐ b ∂κ a, η b (toMeasurable ((η ∘ₖ κ) a) s) < ∞ := by
    refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_
    rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
b : β
hb :
  LT.lt (α := ℝ≥0∞)
    ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono (subset_toMeasurable _ _)).trans_lt hb

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LT.lt (α := ℝ≥0∞)
                    ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
                        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
                      ℝ≥0∞)
                    (∞ : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
                    (∞ : ℝ≥0∞))
                x}
            x}
      a_1
h₂ h₃ :
  ∀ (b : β)
    (hb :
      LT.lt (α := ℝ≥0∞)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
          ℝ≥0∞)
        (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : MeasurableSet s
rw :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a = 0 ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
rw₁ rw₂ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0

Tactic:
rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff (η.measurable_coe hs)]

Premises used: MeasureTheory.lintegral_eq_zero_iff, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t : Set γ) (hst : s ⊆ t) (mt : MeasurableSet t)
    (ht : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h

Premises used: mt, MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0

Tactic:
simp_rw [comp_null a mt] at ht

Premises used: ProbabilityTheory.Kernel.comp_null