awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (f : X →C_c ℝ),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (f : C(X, ℝ)) (hf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K)
  (hf2 : IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)))
  (hf3 :
    tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
  ∃ (f : X →C_c ℝ),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨f, hf1, hf2, hf3⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK pV2 pV1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have obtain : ∀ (f : X →C_c ℝ) (pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K) (pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V)
  (pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
  μ.real K ≤ ν.real K + (↑ε : ℝ)
Tactic: obtain ⟨f, pf1, pf2, pf3⟩ :
      ∃ f : C_c(X, ℝ), Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by
    obtain ⟨f, hf1, hf2, hf3⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK pV2 pV1
    exact ⟨⟨f, hasCompactSupport_def.mpr hf2⟩, hf1, hf3⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
have pos : ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x),
  LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
pos :
  ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x),
    LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
have neg : ∀ (hx : x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
Tactic: have hfV (x : X) : f x ≤ V.indicator 1 x := by
    by_cases hx : x ∈ tsupport f
    · simp [(pf2 hx), (pf3 x).2]
    · simp [image_eq_zero_of_notMem_tsupport hx, Set.indicator_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
x : X
⊢ LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
have pos : ∀ (hx : x ∈ K), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: by_cases hx : x ∈ K
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
x : X
pos : ∀ (hx : x ∈ K), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
have neg : ∀ (hx : x ∉ K), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: by_cases hx : x ∈ K
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: have hfK (x : X) : K.indicator 1 x ≤ f x := by
    by_cases hx : x ∈ K
    · simp [hx, pf1 hx]
    · simp [hx, (pf3 x).1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have refine : Integrable (ε := ℝ) (K.indicator 1) μ
Tactic: refine integral_mono ?_ f.integrable hfK
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)
have refine : Integrable (ε := ℝ) (V.indicator 1) ν
Tactic: refine integral_mono f.integrable ?_ hfV
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)
have ha : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
ha : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)
have hb : HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≠ ∞
Tactic: rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
ha : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hb : HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≠ ∞
ha₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)
have hb₁ : (↑ε : ℝ≥0∞) ≠ ∞
Tactic: rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have K₁ : LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: calc
    μ.real K = ∫ x, K.indicator 1 x ∂μ := integral_indicator_one hK.measurableSet |>.symm
    _ ≤ ∫ x, f x ∂μ := by
      refine integral_mono ?_ f.integrable hfK
      exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet
    _ ≤ ∫ x, f x ∂ν := hμν f
    _ ≤ ∫ x, V.indicator 1 x ∂ν := by
      refine integral_mono f.integrable ?_ hfV
      exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet
    _ ≤ (ν K).toReal + ↑ε := by
      rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
      all_goals finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K₁ : LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have K₂ : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)
Tactic: calc
    μ.real K = ∫ x, K.indicator 1 x ∂μ := integral_indicator_one hK.measurableSet |>.symm
    _ ≤ ∫ x, f x ∂μ := by
      refine integral_mono ?_ f.integrable hfK
      exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet
    _ ≤ ∫ x, f x ∂ν := hμν f
    _ ≤ ∫ x, V.indicator 1 x ∂ν := by
      refine integral_mono f.integrable ?_ hfV
      exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet
    _ ≤ (ν K).toReal + ↑ε := by
      rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
      all_goals finiteness