awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : AEMeasurable X (P.restrict s)
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
have pos₁ : Measurable P⁻[X|mΩ]
Tactic: rw [lintegral_const_mul, lintegral_const_mul'', setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
pos : ∀ (hm : mΩ ≤ mΩ₀), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have neg : HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
Tactic: simp_rw [condLExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
have neg : ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have neg : HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
Tactic: simp_rw [condLExp_of_not_sigmaFinite hm hσ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
have neg : ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
have pos : c • P⁻[X|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[c • X|mΩ]
Tactic: apply ae_le_of_ae_le_trim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (c • P⁻[X|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P
Tactic: refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
have pos : c * ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
Tactic: rw [lintegral_const_mul' _ _ hc, lintegral_const_mul' _ _ hc, setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : c * ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
have pos₁ : c * ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P
Tactic: rw [lintegral_const_mul' _ _ hc, lintegral_const_mul' _ _ hc, setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : c * ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
pos₁ : c * ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
have pos₂ : c * ∫⁻ (ω : Ω) in s, X ω ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P
Tactic: rw [lintegral_const_mul' _ _ hc, lintegral_const_mul' _ _ hc, setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have neg : (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
Tactic: simp_rw [condLExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : ¬mΩ ≤ mΩ₀
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
have neg : ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have neg : (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
Tactic: simp_rw [condLExp_of_not_sigmaFinite hm hσ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
have neg : ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]
have pos : ∀ (s : Set Ω),
  MeasurableSet s → ∫⁻ (ω : Ω) in s, (∑' (i : ι), P⁻[X i|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (∑' (i : ι), X i) ω ∂P
Tactic: refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, (∑' (i : ι), P⁻[X i|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (∑' (i : ι), X i) ω ∂P
have pos : ∫⁻ (ω : Ω) in s, ∑' (i : ι), P⁻[X i|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P
Tactic: simp only [ENNReal.tsum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P
have pos : Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)
Tactic: rw [lintegral_tsum (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, ∑' (i : ι), P⁻[X i|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P
have pos : Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)
Tactic: repeat rw [lintegral_tsum (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)
have pos : ∀ (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P = ∫⁻ (a : Ω) in s, X i a ∂P
Tactic: congr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ P⁻[∑ i ∈ s, X i|mΩ] =ᶠ[ae P] ∑ i ∈ s, P⁻[X i|mΩ]
have h : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, X i) (∑' (i : ↥s), X (↑i : ι))
Tactic: convert! condLExp_tsum mΩ (fun i : s ↦ hX i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
h : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, X i) (∑' (i : ↥s), X (↑i : ι))
⊢ P⁻[∑ i ∈ s, X i|mΩ] =ᶠ[ae P] ∑ i ∈ s, P⁻[X i|mΩ]
have h₁ : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, P⁻[X i|mΩ]) (∑' (i : ↥s), P⁻[X (↑i : ι)|mΩ])
Tactic: convert! condLExp_tsum mΩ (fun i : s ↦ hX i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have obtain : ∀ (η : ℝ≥0) (η_pos : 0 < η)
  (hη :
    ∀ (s : Set α),
      (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε),
  ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
Tactic: obtain ⟨η, η_pos, hη⟩ :
      ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε :=
    exists_eLpNorm_indicator_le hp c hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have ηpos : 0 < (↑η : ℝ≥0∞)
Tactic: have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have obtain : ∀ (V : Set α) (sV : V ⊇ s) (V_open : IsOpen[inst] V)
  (h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)),
  ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
Tactic: obtain ⟨V, sV, V_open, h'V, hV⟩ : ∃ (V : Set α), V ⊇ s ∧ IsOpen V ∧ μ V < ∞ ∧ μ (V \ s) < η :=
    s_closed.measurableSet.exists_isOpen_diff_lt hs ηpos.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have hsv : s ⊆ v
Tactic: have hsv : s ⊆ v := subset_inter hsu sV
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμv : μ v < ∞ := (measure_mono inter_subset_right).trans_lt h'V
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
have obtain : ∀ (g : C(α, ℝ)) (hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ) (hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s)
  (hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)),
  ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
Tactic: obtain ⟨g, hgv, hgs, hg_range⟩ :=
    exists_continuous_zero_one_of_isClosed (u_open.inter V_open).isClosed_compl s_closed
      (disjoint_compl_left_iff.2 hsv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
x : α
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
have rw : Eq (α := ℝ) (|(g : (a : α) → ℝ) x| : ℝ) ((g : (a : α) → ℝ) x : ℝ)
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]