awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atTop (𝓝 1)
have h : ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)) (h_mono : Monotone (f (a, t))),
  Tendsto (f (a, t)) atTop (𝓝 1)
Tactic: filter_upwards [this, hf.mono a] with t ht h_mono
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
h_mono : Monotone (f (a, t))
⊢ Tendsto (f (a, t)) atTop (𝓝 1)
have h : Tendsto (f (a, t) ∘ Nat.cast) atTop (𝓝 1)
Tactic: rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atTop (𝓝 1)
have suffices : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
Tactic: suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) n) atTop (𝓝 1) by
    filter_upwards [this, hf.mono a] with t ht h_mono
    rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]
    exact ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β | (fun (c : β) ↦ Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (↑m : ℚ)) atTop (𝓝 1)) x} x →
        Membership.mem (γ := Set β)
          {x : β | (fun (t : β) ↦ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)) x} x}
    a_1
Tactic: filter_upwards [hf.tendsto_one_of_monotone a Nat.cast Nat.mono_cast tendsto_natCast_atTop_atTop]
    with x hx using hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β | (fun (c : β) ↦ Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (↑m : ℚ)) atTop (𝓝 1)) x} x →
          Membership.mem (γ := Set β)
            {x : β | (fun (t : β) ↦ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)) x} x}
      a_1
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
have h₁ : ∀ (a_1 : β),
  Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, a_1) (↑m : ℚ)) atTop (𝓝 1) →
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, a_1) (↑n : ℚ)) atTop (𝓝 1)
Tactic: filter_upwards [hf.tendsto_one_of_monotone a Nat.cast Nat.mono_cast tendsto_natCast_atTop_atTop]
    with x hx using hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atBot (𝓝 0)
have h : ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)), Tendsto (f (a, t)) atBot (𝓝 0)
Tactic: filter_upwards [this] with t ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atBot (𝓝 0)
have suffices : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
Tactic: suffices ∀ᵐ t ∂(ν a), Tendsto (fun q : ℚ ↦ f (a, t) (-q)) atTop (𝓝 0) by
    filter_upwards [this] with t ht
    exact tendsto_comp_neg_atTop_iff.mp ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
have h : ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)) (h_mono : Monotone (f (a, t))),
  Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
Tactic: filter_upwards [this, hf.mono a] with t ht h_mono
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
⊢ Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
have h_anti : Antitone (β := ℝ) fun (q : ℚ) ↦ f (a, t) (-q)
Tactic: have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
have suffices : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
Tactic: suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) (-n)) atTop (𝓝 0) by
    filter_upwards [this, hf.mono a] with t ht h_mono
    have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
    exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
have h : ∀ (c : β) (hc : ∀ (q : ℚ), 0 ≤ f (a, c) q) (q : ℚ),
  BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))
Tactic: filter_upwards [hf.nonneg a] with c hc
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))
have h : ∀ (q : ℚ), Membership.mem (γ := Set ℝ) (lowerBounds (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))) 0
Tactic: refine fun q ↦ ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ @Integrable ℝ _ _ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ((ν : (a : α) → Measure β) a)
have rw : MemLp (ε := ℝ) (m0 := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a)
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ MemLp (ε := ℝ) (m0 := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a)
have refine : @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) < ∞
Tactic: refine ⟨(Measurable.iInf fun i ↦ hf.measurable_right a _).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) < ∞
have refine : @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) ≤
  (((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ
Tactic: refine (?_ : _ ≤ (ν a univ : ℝ≥0∞)).trans_lt (measure_lt_top _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) ≤
    (((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ
have refine : ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β), norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) ≤ 1
Tactic: refine (eLpNorm_le_of_ae_bound (C := 1) ?_).trans (by simp)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) ≤ 1
have h : ∀ (t : β) (hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ)))
  (h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q) (h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1),
  norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤ 1
Tactic: filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a]
    with t hbdd_below h_nonneg h_le_one
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤ 1
have h : LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
h : LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
⊢ norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤ 1
have h₁ : LE.le (α := ℝ) 0 (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
have h : BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
Tactic: refine ciInf_le_of_le ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
h : BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
have h₁ : (↑(Ioi q) : Type)
Tactic: refine ciInf_le_of_le ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
h : BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h₁ : (↑(Ioi q) : Type)
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
have h₂ : f (a, t) (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi q) (q + 1) sorry) : ℚ) ≤ 1
Tactic: refine ciInf_le_of_le ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
Tactic: rw [← Monotone.measure_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
rw :
  Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have hs₁ : Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : { r' : ℚ // t < r' }) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))
Tactic: rw [← Monotone.measure_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
rw :
  Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
hs₁ :
  Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : { r' : ℚ // t < r' }) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))
⊢ Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have hsm : ∀ (i : { r' : ℚ // t < r' }), NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ρ
Tactic: rw [← Monotone.measure_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
rw :
  Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
hs₁ :
  Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : { r' : ℚ // t < r' }) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))
hsm : ∀ (i : { r' : ℚ // t < r' }), NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ρ
⊢ Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have hfin : ∃ (i : { r' : ℚ // t < r' }),
  Ne (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Monotone.measure_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
Tactic: rw [← prod_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
have h : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ)) x ↔
    Membership.mem (γ := Set ℝ) (Iic (↑t : ℝ)) x
Tactic: congr with x : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ)) x ↔
    Membership.mem (γ := Set ℝ) (Iic (↑t : ℝ)) x
have h : (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)
Tactic: simp only [mem_iInter, mem_Iic, Subtype.forall]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)
have h : ∀ (h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)), x ≤ (↑t : ℝ)
Tactic: refine ⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)), x ≤ (↑t : ℝ)
⊢ (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)
have h₁ : ∀ (h : x ≤ (↑t : ℝ)) (a : ℚ) (hta : t < a), LE.le (α := ℝ) (↑t : ℝ) (↑a : ℝ)
Tactic: refine ⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)
⊢ x ≤ (↑t : ℝ)
have h₁ : ∀ (q : ℚ) (htq : LT.lt (α := ℝ) (↑t : ℝ) (↑q : ℝ)), t < q
Tactic: refine le_of_forall_lt_rat_imp_le fun q htq ↦ h q ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))
have refine_1 : (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
    ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))
Tactic: refine le_antisymm ?_ ?_