awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f
have refine_1 : ∀ (s : Set α) (hs : MeasurableSet s)
  (hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), IntegrableOn f s (μ.restrict t)
Tactic: refine
    ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite (fun s hs hμts => ?_) fun s hs hμts => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
refine_1 :
  ∀ (s : Set α) (hs : MeasurableSet s)
    (hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableOn f s (μ.restrict t)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f
have refine_2 : ∀ (s : Set α) (hs : MeasurableSet s)
  (hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
Tactic: refine
    ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite (fun s hs hμts => ?_) fun s hs hμts => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn f s (μ.restrict t)
have refine_1 : Integrable f (μ.restrict (s ∩ t))
Tactic: rw [IntegrableOn, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (μ.restrict (s ∩ t))
have hμts₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply hs] at hμts
Cleared hypotheses: hμts
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
have refine_2 : LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: rw [Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
have hμts₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply hs] at hμts
Cleared hypotheses: hμts
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f
have t₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: refine
    ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
      (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) fun s hs _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f =ᶠ[ae (μ.restrict t)] 0
have suffices : f ≤ᶠ[ae (μ.restrict t)] 0 ∧ 0 ≤ᶠ[ae (μ.restrict t)] f
Tactic: suffices h_and : f ≤ᵐ[μ.restrict t] 0 ∧ 0 ≤ᵐ[μ.restrict t] f from
    h_and.1.mp (h_and.2.mono fun x hx1 hx2 => le_antisymm hx2 hx1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f ≤ᶠ[ae (μ.restrict t)] 0 ∧ 0 ≤ᶠ[ae (μ.restrict t)] f
have ae_nonneg_restrict_of_forall_setIntegral_nonneg : f ≤ᶠ[ae (μ.restrict t)] 0
Tactic: refine
    ⟨?_,
      ae_nonneg_restrict_of_forall_setIntegral_nonneg hf_int_finite
        (fun s hs hμs => (hf_zero s hs hμs).symm.le) ht hμt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_neg : 0 ≤ᶠ[ae (μ.restrict t)] -f
⊢ f ≤ᶠ[ae (μ.restrict t)] 0
have refine : ∀ (x : α) (hx : 0 x ≤ (-f) x), f x ≤ 0 x
Tactic: refine h_neg.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_neg : 0 ≤ᶠ[ae (μ.restrict t)] -f
x : α
hx : 0 x ≤ (-f) x
⊢ f x ≤ 0 x
have hx₁ : 0 x ≤ -f x
Tactic: rw [Pi.neg_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f ≤ᶠ[ae (μ.restrict t)] 0
have suffices : 0 ≤ᶠ[ae (μ.restrict t)] -f
Tactic: suffices h_neg : 0 ≤ᵐ[μ.restrict t] -f by
    refine h_neg.mono fun x hx => ?_
    rw [Pi.neg_apply] at hx
    simpa using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] -f
have ae_nonneg_restrict_of_forall_setIntegral_nonneg : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ) 0 (∫ (x : α) in s, (-f) x ∂μ)
Tactic: refine
    ae_nonneg_restrict_of_forall_setIntegral_nonneg (fun s hs hμs => (hf_int_finite s hs hμs).neg)
      (fun s hs hμs => ?_) ht hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, -f x ∂μ)
have rw : LE.le (α := ℝ) (∫ (a : α) in s, f a ∂μ) 0
Tactic: rw [integral_neg, neg_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f =ᶠ[ae (μ.restrict t)] 0
have rcases : ∀ (u : Set E) (u_sep : IsSeparable u) (hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u), f =ᶠ[ae (μ.restrict t)] 0
Tactic: rcases (hf_int_finite t ht hμt.lt_top).aestronglyMeasurable.isSeparable_ae_range with
    ⟨u, u_sep, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
⊢ f =ᶠ[ae (μ.restrict t)] 0
have refine : ∀ (c : StrongDual ℝ E), (ae (μ.restrict t)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (c : (a : E) → ℝ) (f x)) 0
Tactic: refine ae_eq_zero_of_forall_dual_of_isSeparable ℝ u_sep (fun c => ?_) hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
⊢ (ae (μ.restrict t)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (c : (a : E) → ℝ) (f x)) 0
have refine_1 : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (fun (x : α) ↦ (c : (a : E) → ℝ) (f x)) s μ
Tactic: refine ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real ?_ ?_ ht hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (fun (x : α) ↦ (c : (a : E) → ℝ) (f x)) s μ
⊢ (ae (μ.restrict t)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (c : (a : E) → ℝ) (f x)) 0
have refine_2 : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : α) in s, (c : (a : E) → ℝ) (f x) ∂μ) 0
Tactic: refine ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real ?_ ?_ ht hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : α) in s, (c : (a : E) → ℝ) (f x) ∂μ) 0
have refine_2 : Eq (α := ℝ) ((c : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [ContinuousLinearMap.integral_comp_comm c (hf_int_finite s hs hμs), hf_zero s hs hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f =ᶠ[ae (μ.restrict t)] g
have rw : f - g =ᶠ[ae (μ.restrict t)] 0
Tactic: rw [← sub_ae_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
have rw : HSub.hSub (α := E) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ) = 0
Tactic: rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f - g =ᶠ[ae (μ.restrict t)] 0
have hfg' : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
Tactic: have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg_zero s hs hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
⊢ f - g =ᶠ[ae (μ.restrict t)] 0
have hfg_int : ∀ (s : Set α),
  MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ
Tactic: have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
    (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : SigmaFinite μ
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
S : (i : ℕ) → Set α := spanningSets μ
⊢ f =ᶠ[ae μ] 0
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ ⋃ (b : ℕ), spanningSets μ b) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← @Measure.restrict_univ _ _ μ, ← iUnion_spanningSets μ, EventuallyEq, ae_iff,
    Measure.restrict_apply' (MeasurableSet.iUnion (measurableSet_spanningSets μ))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : SigmaFinite μ
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
S : (i : ℕ) → Set α := spanningSets μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ ⋃ (b : ℕ), spanningSets μ b) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Set.inter_iUnion, measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : SigmaFinite μ
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)
have h_meas_n : MeasurableSet (S n)
Tactic: have h_meas_n : MeasurableSet (S n) := measurableSet_spanningSets μ n