awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]

Tactic:
simp [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]
neg : ∀ (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Ω]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]

Tactic:
simp [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (c • P⁻[X|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (c • P⁻[X|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm

Premises used: MeasureTheory.ae_eq_condLExp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos₂ pos₃ : c * ∫⁻ (ω : Ω) in s, X ω ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P

Tactic:
rw [lintegral_const_mul' _ _ hc, lintegral_const_mul' _ _ hc, setLIntegral_condLExp _ _ _ hs]

Premises used: MeasureTheory.lintegral_const_mul', MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]
neg : ∀ (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Ω]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω₀
neg : (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω₀
neg : ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω₀
⊢ ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]
neg : ∀ (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Ω]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
neg : (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
neg : ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) 0 (∑' (i : ι), 0)

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
⊢ ∀ (a : Ω), Eq (α := ℝ≥0∞) (0 a) ((∑' (i : ι), 0) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
⊢ Measurable.{u_1, 0} (α := Ω) (β := ℝ≥0∞) (∑' (i : ι), P⁻[X i|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
pos :
  ∀ (s : Set Ω),
    MeasurableSet s → ∫⁻ (ω : Ω) in s, (∑' (i : ι), P⁻[X i|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (∑' (i : ι), X i) ω ∂P
⊢ P⁻[∑' (i : ι), X i|mΩ] =ᶠ[ae P] ∑' (i : ι), P⁻[X i|mΩ]

Tactic:
refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm

Premises used: MeasureTheory.ae_eq_condLExp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos : ∫⁻ (ω : Ω) in s, ∑' (i : ι), P⁻[X i|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P
⊢ ∫⁻ (ω : Ω) in s, (∑' (i : ι), P⁻[X i|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (∑' (i : ι), X i) ω ∂P

Tactic:
simp only [ENNReal.tsum_apply]

Premises used: ENNReal.tsum_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 : ι), AEMeasurable P⁻[X i|mΩ] (P.restrict s)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 : ι), AEMeasurable (X i) (P.restrict s)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos : Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)
⊢ ∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P

Tactic:
rw [lintegral_tsum (by measurability)]

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos : Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)
⊢ ∫⁻ (ω : Ω) in s, ∑' (i : ι), P⁻[X i|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, ∑' (i : ι), X i ω ∂P

Tactic:
repeat rw [lintegral_tsum (by measurability)]

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos : ∀ (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P = ∫⁻ (a : Ω) in s, X i a ∂P
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : Ω) in s, P⁻[X i|mΩ] a ∂P) (∑' (i : ι), ∫⁻ (a : Ω) in s, X i a ∂P)

Tactic:
congr with i
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 = ∫⁻ (a : Ω) in s, X i a ∂P

Tactic:
setLIntegral_condLExp hm P (X i) hs

Premises used: MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 = ∫⁻ (a : Ω) in s, X i a ∂P

Tactic:
exact setLIntegral_condLExp hm P (X i) hs

Premises used: MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]

Tactic:
condLExp_tsum mΩ (fun i : s ↦ hX i)

Premises used: Subtype.val, MeasureTheory.condLExp_tsum
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 : ι))
h₁ : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, P⁻[X i|mΩ]) (∑' (i : ↥s), P⁻[X (↑i : ι)|mΩ])
⊢ P⁻[∑ i ∈ s, X i|mΩ] =ᶠ[ae P] ∑ i ∈ s, P⁻[X i|mΩ]

Tactic:
convert! condLExp_tsum mΩ (fun i : s ↦ hX i)

Premises used: Subtype.val, MeasureTheory.condLExp_tsum
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, X i) (∑' (i : ↥s), X (↑i : ι))

Tactic:
simp [Finset.sum_attach]

Premises used: Finset.sum_attach
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) (∑ i ∈ s, P⁻[X i|mΩ]) (∑' (i : ↥s), P⁻[X (↑i : ι)|mΩ])

Tactic:
simp [Finset.sum_attach _ (f := (P⁻[X ·|mΩ]))]

Premises used: Finset.sum_attach, MeasureTheory.condLExp
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε

Tactic:
exists_eLpNorm_indicator_le hp c hε

Premises used: MeasureTheory.exists_eLpNorm_indicator_le
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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
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 μ
⊢ ∃ (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ε

Premises used: MeasureTheory.exists_eLpNorm_indicator_le
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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 μ ≤ ε
⊢ 0 < (↑η : ℝ≥0∞)

Tactic:
have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_pos
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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 ⊇ s,
    IsOpen[inst] V ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)

Tactic:
s_closed.measurableSet.exists_isOpen_diff_lt hs ηpos.ne'

Premises used: IsClosed.measurableSet, MeasurableSet.exists_isOpen_diff_lt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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∞)
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 μ
⊢ ∃ (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'

Premises used: IsClosed.measurableSet, MeasurableSet.exists_isOpen_diff_lt, LT.lt.ne', Set
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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
⊢ s ⊆ v

Tactic:
have hsv : s ⊆ v := subset_inter hsu sV
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμv : μ v < ∞ := (measure_mono inter_subset_right).trans_lt h'V
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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∞)
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 μ
⊢ ∃ (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)

Premises used: Iff.mpr, exists_continuous_zero_one_of_isClosed, IsOpen.isClosed_compl, disjoint_compl_left_iff, IsOpen.inter
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
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 : α
rw : Eq (α := ℝ) (|(g : (a : α) → ℝ) x| : ℝ) ((g : (a : α) → ℝ) x : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]

Premises used: And.left, abs_of_nonneg, Real.norm_eq_abs