-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt (hf : IsRatCondKernelCDFAux f κ ν)
    [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) (q : ℚ) {A : Set β} (hA : MeasurableSet A) :
    ∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a) = (κ a (A ×ˢ Iic (q : ℝ))).toReal

Proof state:
case refine_2.refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (fun c => f (a, c) q) ≤ᶠ[ae (ν a)] fun t => ⨅ r, f (a, t) ↑r

Tactic:
filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal
⊢ ⨅ r, ((κ a) (A ×ˢ Iic ↑↑r)).toReal = (⨅ r, (κ a) (A ×ˢ Iic ↑↑r)).toReal

Tactic:
exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ∫ (c : β) in A, f (a, c) ↑r ∂ν a

Tactic:
refine setIntegral_mono_ae ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun t => ⨅ r', f (a, t) ↑r') A (ν a)

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun c => f (a, c) ↑r) A (ν a)

case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ (fun t => ⨅ r', f (a, t) ↑r') ≤ᶠ[ae (ν a)] fun c => f (a, c) ↑r

Proof state:
case refine_2.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (fun t => ⨅ r, f (a, t) ↑r) A (ν a)

Tactic:
exact (hf.integrable_iInf_rat_gt _ _).integrableOn

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal
⊢ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑q)).toReal

Tactic:
calc ∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a)
  ≤ ⨅ r : Ioi q, (κ a (A ×ˢ Iic (r : ℝ))).toReal := le_ciInf h
_ = (κ a (A ×ˢ Iic (q : ℝ))).toReal := by
    rw [← Measure.iInf_rat_gt_prod_Iic hA q]
    exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal

Tactic:
intro r

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal

Proof state:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun t => ⨅ r', f (a, t) ↑r') A (ν a)

Tactic:
exact (hf.integrable_iInf_rat_gt _ _).integrableOn

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal
⊢ ⨅ r, ((κ a) (A ×ˢ Iic ↑↑r)).toReal = ((κ a) (A ×ˢ Iic ↑q)).toReal

Tactic:
rw [← Measure.iInf_rat_gt_prod_Iic hA q]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑↑r)).toReal
⊢ ⨅ r, ((κ a) (A ×ˢ Iic ↑↑r)).toReal = (⨅ r, (κ a) (A ×ˢ Iic ↑↑r)).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a = ((κ a) (A ×ˢ Iic ↑q)).toReal

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑q)).toReal

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ((κ a) (A ×ˢ Iic ↑q)).toReal ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a

Proof state:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun c => f (a, c) ↑r) A (ν a)

Tactic:
exact (hf.integrable _ _).integrableOn

Result:
no goals