[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
by_cases hfint : Integrable f μ
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
case neg
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
rw [condexp_undef hfint, integral_undef hfint]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : ¬Integrable f
⊢ 0 =ᵐ[μ] fun x => 0
[PROOFSTEP]
rfl
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
⊢ μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
[PROOFSTEP]
refine'
  (ae_eq_condexp_of_forall_set_integral_eq hle₂ hfint (fun s _ hs => integrableOn_const.2 (Or.inr hs))
      (fun s hms hs => _) stronglyMeasurable_const.aeStronglyMeasurable').symm
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
rw [set_integral_const]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Integrable f
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hfint 
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
[PROOFSTEP]
refine' Memℒp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ _ _ _ hfint _
[GOAL]
case pos.refine'_1
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ AEStronglyMeasurable' m₁ f μ
[PROOFSTEP]
exact ⟨f, hf, EventuallyEq.rfl⟩
[GOAL]
case pos.refine'_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ →
        ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator s_1 (fun x => c) x ∂μ =
          ∫ (x : Ω) in s, Set.indicator s_1 (fun x => c) x ∂μ
[PROOFSTEP]
intro c t hmt _
[GOAL]
case pos.refine'_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator t (fun x => c) x ∂μ =
    ∫ (x : Ω) in s, Set.indicator t (fun x => c) x ∂μ
[PROOFSTEP]
rw [Indep_iff] at hindp 
[GOAL]
case pos.refine'_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), Set.indicator t (fun x => c) x ∂μ =
    ∫ (x : Ω) in s, Set.indicator t (fun x => c) x ∂μ
[PROOFSTEP]
rw [integral_indicator (hle₁ _ hmt), set_integral_const, smul_smul, ← ENNReal.toReal_mul, mul_comm, ← hindp _ _ hmt hms,
  set_integral_indicator (hle₁ _ hmt), set_integral_const, Set.inter_comm]
[GOAL]
case pos.refine'_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Memℒp f 1 →
        Memℒp g 1 →
          StronglyMeasurable f →
            StronglyMeasurable g →
              ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
                ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ →
                  ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ
[PROOFSTEP]
intro u v _ huint hvint hu hv hu_eq hv_eq
[GOAL]
case pos.refine'_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Memℒp u 1
hvint : Memℒp v 1
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
[PROOFSTEP]
rw [memℒp_one_iff_integrable] at huint hvint 
[GOAL]
case pos.refine'_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : Integrable u
hvint : Integrable v
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
hv_eq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
[PROOFSTEP]
rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq, integral_add' huint.integrableOn hvint.integrableOn]
[GOAL]
case pos.refine'_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
have heq₁ :
  (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ) = (fun f : Lp E 1 μ => ∫ x, f x ∂μ) ∘ Submodule.subtypeL _ :=
  by
  refine' funext fun f => integral_congr_ae _
  simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]; norm_cast
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
[PROOFSTEP]
refine' funext fun f => integral_congr_ae _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ (fun x => ↑↑↑f x) =ᵐ[μ] fun x => ↑↑(↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)) f) x
[PROOFSTEP]
simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ (fun x => ↑↑↑f x) =ᵐ[μ] fun x => ↑↑↑f x
[PROOFSTEP]
norm_cast
[GOAL]
case pos.refine'_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
have heq₂ :
  (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ) =
    (fun f : Lp E 1 μ => ∫ x in s, f x ∂μ) ∘ Submodule.subtypeL _ :=
  by
  refine' funext fun f => integral_congr_ae (ae_restrict_of_ae _)
  simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
  exact eventually_of_forall fun _ => (by trivial)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
[PROOFSTEP]
refine' funext fun f => integral_congr_ae (ae_restrict_of_ae _)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ ∀ᵐ (x : Ω) ∂μ, (fun x => ↑↑↑f x) x = (fun x => ↑↑(↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)) f) x) x
[PROOFSTEP]
simp_rw [Submodule.coe_subtypeL', Submodule.coeSubtype]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
⊢ ∀ᵐ (x : Ω) ∂μ, True
[PROOFSTEP]
exact eventually_of_forall fun _ => (by trivial)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f✝ : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f✝
hindp : Indep m₁ m₂
hfint : Memℒp f✝ 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
f : { x // x ∈ lpMeas E ℝ m₁ 1 μ }
x✝ : Ω
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case pos.refine'_4
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ IsClosed {f | ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
[PROOFSTEP]
refine' isClosed_eq (Continuous.const_smul _ _) _
[GOAL]
case pos.refine'_4.refine'_1
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous fun f => ∫ (x : Ω), ↑↑↑f x ∂μ
[PROOFSTEP]
rw [heq₁]
[GOAL]
case pos.refine'_4.refine'_1
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous ((fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)))
[PROOFSTEP]
exact continuous_integral.comp (ContinuousLinearMap.continuous _)
[GOAL]
case pos.refine'_4.refine'_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ
[PROOFSTEP]
rw [heq₂]
[GOAL]
case pos.refine'_4.refine'_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
heq₁ : (fun f => ∫ (x : Ω), ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω), ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
heq₂ :
  (fun f => ∫ (x : Ω) in s, ↑↑↑f x ∂μ) = (fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ))
⊢ Continuous ((fun f => ∫ (x : Ω) in s, ↑↑f x ∂μ) ∘ ↑(Submodule.subtypeL (lpMeas E ℝ m₁ 1 μ)))
[PROOFSTEP]
exact (continuous_set_integral _).comp (ContinuousLinearMap.continuous _)
[GOAL]
case pos.refine'_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
⊢ ∀ ⦃f g : Ω → E⦄,
    f =ᵐ[μ] g →
      Memℒp f 1 →
        ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ →
          ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ
[PROOFSTEP]
intro u v huv _ hueq
[GOAL]
case pos.refine'_5
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : Memℒp u 1
hueq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ
[PROOFSTEP]
rwa [← integral_congr_ae huv, ← (set_integral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (Measure.trim μ hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂
hfint : Memℒp f 1
s : Set Ω
hms : MeasurableSet s
hs : ↑↑μ s < ⊤
u v : Ω → E
huv : u =ᵐ[μ] v
a✝ : Memℒp u 1
hueq : ENNReal.toReal (↑↑μ s) • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
[PROOFSTEP]
filter_upwards [huv] with x hx _ using hx
