awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (SProd.sprod (β := Set Ω) s Set.univ) ρ
rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s, @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) Set.univ) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s, @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂ρ)

Tactic:
rw [← setIntegral_condKernel hs MeasurableSet.univ hf]

Premises used: MeasureTheory.Measure.setIntegral_condKernel, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (SProd.sprod (β := Set Ω) s Set.univ) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s, @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) Set.univ) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)

Tactic:
simp_rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (SProd.sprod (α := Set β) Set.univ t) ρ
rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (b : β),
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (b : β) in Set.univ,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β),
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂ρ)

Tactic:
rw [← setIntegral_condKernel MeasurableSet.univ ht hf]

Premises used: MeasureTheory.Measure.setIntegral_condKernel, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (SProd.sprod (α := Set β) Set.univ t) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β),
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (b : β) in Set.univ,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)

Tactic:
simp_rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f ρ
⊢ AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [← ρ.disintegrate ρ.condKernel] at hf

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
rw : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
| Integrable f ρ

Tactic:
rw [← ρ.disintegrate ρ.condKernel]

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
conv_rhs :
  (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
rw rw₁ :
  (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    (∀ᵐ (x : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (y : Ω) ↦ f (x, y)) ((ρ.condKernel : (a : α) → Measure Ω) x)) ∧
      Integrable (ε := ℝ)
        (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst
⊢ (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [Measure.integrable_compProd_iff hf]

Premises used: MeasureTheory.Measure.integrable_compProd_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ AEStronglyMeasurable f ρ

Tactic:
have hf_ae : AEStronglyMeasurable f ρ := hf_int.1
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Premises used: MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
hf_int₁ :
  (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
⊢ AEStronglyMeasurable f ρ

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Premises used: MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)

Tactic:
hf_int.1

Premises used: And.left
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)

Tactic:
exact hf_int.1

Premises used: And.left
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst

Tactic:
hf_int.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst

Tactic:
exact hf_int.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦
      Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)))
    ρ.fst

Tactic:
hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.integral_condKernel, And.left, MeasureTheory.Integrable.integral_norm_condKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
refine :
  ∀ᵐ (a : α) ∂ρ.fst,
    ‖Norm.norm.{u_3} (E := E)
          (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ f (a, y))‖ ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ ‖f (a, y)‖)
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦
      Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)))
    ρ.fst

Tactic:
refine hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.integral_condKernel, And.left, MeasureTheory.Integrable.integral_norm_condKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    ‖Norm.norm.{u_3} (E := E)
          (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ f (a, y))‖ ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ ‖f (a, y)‖)

Tactic:
Filter.Eventually.of_forall fun x ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
refine :
  ∀ (x : α),
    ‖Norm.norm.{u_3} (E := E)
          (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))‖ ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    ‖Norm.norm.{u_3} (E := E)
          (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ f (a, y))‖ ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ ‖f (a, y)‖)

Tactic:
refine Filter.Eventually.of_forall fun x ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
rw :
  Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
⊢ ‖Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))‖ ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)

Tactic:
rw [norm_norm]

Premises used: norm_norm
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)

Tactic:
(norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm

Premises used: LE.le.trans_eq, MeasureTheory.norm_integral_le_integral_norm, Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
refine : LE.le (α := ℝ) 0 (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (a : Ω) ↦ ‖f (x, a)‖)
⊢ Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)

Tactic:
refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm

Premises used: LE.le.trans_eq, MeasureTheory.norm_integral_le_integral_norm, Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ LE.le (α := ℝ) 0 (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (a : Ω) ↦ ‖f (x, a)‖)

Tactic:
integral_nonneg_of_ae (Filter.Eventually.of_forall fun y ↦ norm_nonneg _)

Premises used: Prod.mk, Filter.Eventually.of_forall, MeasureTheory.integral_nonneg_of_ae, norm_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ LE.le (α := ℝ) 0 (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (a : Ω) ↦ ‖f (x, a)‖)

Tactic:
exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun y ↦ norm_nonneg _)

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_nonneg_of_ae, norm_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Integral
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ Integrable.{u_3, u_1} (ε := E)
    (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ρ.fst

Tactic:
(integrable_norm_iff hf_int.1.integral_condKernel).mp hf_int.norm_integral_condKernel

Premises used: MeasureTheory.Integrable.norm_integral_condKernel, MeasureTheory.integrable_norm_iff, MeasureTheory.AEStronglyMeasurable.integral_condKernel, And.left, Iff.mp
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable (β := ℝ) fun (a : α) ↦ (↑(f a) : ℝ → ℝ) q
hf_bot : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (m0 := Real.measurableSpace) (f a).measure
simp_rw : ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(f a) : ℝ → ℝ) i)
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (range Iic) s →
      Measurable (β := ℝ≥0∞) fun (a : α) ↦ ((f a).measure : (a : Set ℝ) → ℝ≥0∞) s

Tactic:
simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]

Premises used: Set.forall_mem_range, sub_zero, StieltjesFunction.measure_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable (β := ℝ) fun (a : α) ↦ (↑(f a) : ℝ → ℝ) q
hf_bot : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (m0 := Real.measurableSpace) (f a).measure
⊢ ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(f a) : ℝ → ℝ) i)

Tactic:
fun _ ↦ (hf _).ennreal_ofReal

Premises used: Measurable.ennreal_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable (β := ℝ) fun (a : α) ↦ (↑(f a) : ℝ → ℝ) q
hf_bot : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (m0 := Real.measurableSpace) (f a).measure
⊢ ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(f a) : ℝ → ℝ) i)

Tactic:
exact fun _ ↦ (hf _).ennreal_ofReal

Premises used: Measurable.ennreal_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
mp : IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) → IsRatStieltjesPoint f a
mpr : IsRatStieltjesPoint f a → IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a)
⊢ IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) ↔ IsRatStieltjesPoint f a

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) → IsRatStieltjesPoint f a

Tactic:
fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero, ProbabilityTheory.IsRatStieltjesPoint.mk, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) → IsRatStieltjesPoint f a

Tactic:
exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint f a → IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a)

Tactic:
fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero, ProbabilityTheory.IsRatStieltjesPoint.mk, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq