[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (a • s)
[PROOFSTEP]
rw [← preimage_smul_inv]
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
[PROOFSTEP]
exact measurable_const_smul _ hs
[GOAL]
G₀ : Type u_1
α : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulAction G₀ α
inst✝² : MeasurableSpace G₀
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
[PROOFSTEP]
rw [← preimage_smul_inv₀ ha]
[GOAL]
G₀ : Type u_1
α : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulAction G₀ α
inst✝² : MeasurableSpace G₀
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
[PROOFSTEP]
exact measurable_const_smul _ hs
[GOAL]
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)
case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
[PROOFSTEP]
exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]


[GOAL]
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddCommGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F
hS : NullMeasurableSet s
h : ↑↑μ F < ↑↑μ s
⊢ ∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)
[PROOFSTEP]
contrapose! h
[GOAL]
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddCommGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F
hS : NullMeasurableSet s
h : ∀ (x y : L), x ≠ y → Disjoint (x +ᵥ s) (y +ᵥ s)
⊢ ↑↑μ s ≤ ↑↑μ F
[PROOFSTEP]
exact
  ((fund.measure_eq_tsum _).trans
        (measure_iUnion₀ (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).aedisjoint) fun _ =>
            (hS.vadd _).inter fund.nullMeasurableSet).symm).trans_le
    (measure_mono <| Set.iUnion_subset fun _ => Set.inter_subset_right _ _)
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ ∃ x x_1, ↑x ∈ s
[PROOFSTEP]
have h_vol : μ F < μ ((2⁻¹ : ℝ) • s) :=
  by
  rw [addHaar_smul_of_nonneg μ (by norm_num : 0 ≤ (2 : ℝ)⁻¹) s, ←
    mul_lt_mul_right (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (pow_ne_top two_ne_top), mul_right_comm,
    ofReal_pow (by norm_num : 0 ≤ (2 : ℝ)⁻¹), ← ofReal_inv_of_pos zero_lt_two]
  norm_num
  rwa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero two_ne_top, one_pow, one_mul]
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ ↑↑μ F < ↑↑μ (2⁻¹ • s)
[PROOFSTEP]
rw [addHaar_smul_of_nonneg μ (by norm_num : 0 ≤ (2 : ℝ)⁻¹) s, ←
  mul_lt_mul_right (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (pow_ne_top two_ne_top), mul_right_comm,
  ofReal_pow (by norm_num : 0 ≤ (2 : ℝ)⁻¹), ← ofReal_inv_of_pos zero_lt_two]
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ ↑↑μ F * 2 ^ finrank ℝ E < (ENNReal.ofReal 2)⁻¹ ^ finrank ℝ E * 2 ^ finrank ℝ E * ↑↑μ s
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
⊢ ↑↑μ F * 2 ^ finrank ℝ E < 2⁻¹ ^ finrank ℝ E * 2 ^ finrank ℝ E * ↑↑μ s
[PROOFSTEP]
rwa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero two_ne_top, one_pow, one_mul]
[GOAL]
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
⊢ ∃ x x_1, ↑x ∈ s
[PROOFSTEP]
obtain ⟨x, y, hxy, h⟩ := exists_pair_mem_lattice_not_disjoint_vadd fund ((h_conv.smul _).nullMeasurableSet _) h_vol
[GOAL]
case intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
⊢ ∃ x x_1, ↑x ∈ s
[PROOFSTEP]
obtain ⟨_, ⟨v, hv, rfl⟩, w, hw, hvw⟩ := Set.not_disjoint_iff.mp h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : v ∈ 2⁻¹ • s
w : E
hw : w ∈ 2⁻¹ • s
hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v
⊢ ∃ x x_1, ↑x ∈ s
[PROOFSTEP]
refine' ⟨x - y, sub_ne_zero.2 hxy, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : v ∈ 2⁻¹ • s
w : E
hw : w ∈ 2⁻¹ • s
hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v
⊢ ↑(x - y) ∈ s
[PROOFSTEP]
rw [Set.mem_inv_smul_set_iff₀ (two_ne_zero' ℝ)] at hv hw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v
⊢ ↑(x - y) ∈ s
[PROOFSTEP]
simp_rw [AddSubgroup.vadd_def, vadd_eq_add, add_comm _ w, ← sub_eq_sub_iff_add_eq_add, ← AddSubgroup.coe_sub] at hvw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ ↑(x - y) ∈ s
[PROOFSTEP]
rw [← hvw, ← inv_smul_smul₀ (two_ne_zero' ℝ) (_ - _), smul_sub, sub_eq_add_neg, smul_add]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 2⁻¹ • 2 • w + 2⁻¹ • -(2 • v) ∈ s
[PROOFSTEP]
refine' h_conv hw (h_symm _ hv) _ _ _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_3
E : Type u_1
L✝ : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsAddHaarMeasure μ
L : AddSubgroup E
inst✝ : Countable { x // x ∈ L }
fund : IsAddFundamentalDomain { x // x ∈ L } F
h✝ : ↑↑μ F * 2 ^ finrank ℝ E < ↑↑μ s
h_symm : ∀ (x : E), x ∈ s → -x ∈ s
h_conv : Convex ℝ s
h_vol : ↑↑μ F < ↑↑μ (2⁻¹ • s)
x y : { x // x ∈ L }
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 2⁻¹ + 2⁻¹ = 1
[PROOFSTEP]
norm_num


[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : ¬m ≤ m0
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : ¬m ≤ m0
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
simp_rw [condexp_of_not_le hm]
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : ¬m ≤ m0
⊢ 0 =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
by_cases hμm : SigmaFinite (μ.trim hm)
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
simp_rw [condexp_of_not_sigmaFinite hm hμm]
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ 0 =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
haveI : SigmaFinite (μ.trim hm) := hμm
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
have : SigmaFinite ((μ.restrict s).trim hm) :=
  by
  rw [← restrict_trim hm _ hs]
  exact Restrict.sigmaFinite _ s
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
[PROOFSTEP]
rw [← restrict_trim hm _ hs]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ SigmaFinite (Measure.restrict (Measure.trim μ hm) s)
[PROOFSTEP]
exact Restrict.sigmaFinite _ s
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
by_cases hf_int : Integrable f μ
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : ¬Integrable f
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : ¬Integrable f
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
rw [condexp_undef hf_int]
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] 0
[PROOFSTEP]
refine' ae_eq_of_forall_set_integral_eq_of_sigmaFinite' hm _ _ _ _ _
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑(Measure.restrict μ s) s_1 < ⊤ → IntegrableOn (μ[f|m]) s_1
[PROOFSTEP]
exact fun t _ _ => integrable_condexp.integrableOn.integrableOn
[GOAL]
case pos.refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑(Measure.restrict μ s) s_1 < ⊤ → IntegrableOn 0 s_1
[PROOFSTEP]
exact fun t _ _ => (integrable_zero _ _ _).integrableOn
[GOAL]
case pos.refine'_3
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑(Measure.restrict μ s) s_1 < ⊤ →
        ∫ (x : α) in s_1, (μ[f|m]) x ∂Measure.restrict μ s = ∫ (x : α) in s_1, OfNat.ofNat 0 x ∂Measure.restrict μ s
[PROOFSTEP]
intro t ht _
[GOAL]
case pos.refine'_3
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑(Measure.restrict μ s) t < ⊤
⊢ ∫ (x : α) in t, (μ[f|m]) x ∂Measure.restrict μ s = ∫ (x : α) in t, OfNat.ofNat 0 x ∂Measure.restrict μ s
[PROOFSTEP]
rw [Measure.restrict_restrict (hm _ ht), set_integral_condexp hm hf_int (ht.inter hs), ←
  Measure.restrict_restrict (hm _ ht)]
[GOAL]
case pos.refine'_3
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑(Measure.restrict μ s) t < ⊤
⊢ ∫ (x : α) in t, f x ∂Measure.restrict μ s = ∫ (x : α) in t, OfNat.ofNat 0 x ∂Measure.restrict μ s
[PROOFSTEP]
refine' set_integral_congr_ae (hm _ ht) _
[GOAL]
case pos.refine'_3
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑(Measure.restrict μ s) t < ⊤
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, x ∈ t → f x = OfNat.ofNat 0 x
[PROOFSTEP]
filter_upwards [hf] with x hx _ using hx
[GOAL]
case pos.refine'_4
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ AEStronglyMeasurable' m (μ[f|m]) (Measure.restrict μ s)
[PROOFSTEP]
exact stronglyMeasurable_condexp.aeStronglyMeasurable'
[GOAL]
case pos.refine'_5
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
hf_int : Integrable f
⊢ AEStronglyMeasurable' m 0 (Measure.restrict μ s)
[PROOFSTEP]
exact stronglyMeasurable_zero.aeStronglyMeasurable'
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : ¬m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : ¬m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
simp_rw [condexp_of_not_le hm, Set.indicator_zero']
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : ¬m ≤ m0
⊢ 0 =ᵐ[μ] 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
have hsf_zero : ∀ g : α → E, g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g := fun g =>
  indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs)
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᵐ[Measure.restrict μ sᶜ] 0 → Set.indicator s g =ᵐ[μ] g
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
refine' ((hsf_zero (μ[f|m]) (condexp_ae_eq_restrict_zero hs.compl hf)).trans _).symm
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[Measure.restrict μ sᶜ] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᵐ[Measure.restrict μ sᶜ] 0 → Set.indicator s g =ᵐ[μ] g
⊢ μ[f|m] =ᵐ[μ] μ[Set.indicator s f|m]
[PROOFSTEP]
exact condexp_congr_ae (hsf_zero f hf).symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
simp_rw [condexp_of_not_le hm, Set.indicator_zero']
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ 0 =ᵐ[μ] 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
by_cases hμm : SigmaFinite (μ.trim hm)
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
simp_rw [condexp_of_not_sigmaFinite hm hμm, Set.indicator_zero']
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ 0 =ᵐ[μ] 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
haveI : SigmaFinite (μ.trim hm) := hμm
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
have : s.indicator (μ[f|m]) =ᵐ[μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) := by
  rw [Set.indicator_self_add_compl s f]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
[PROOFSTEP]
rw [Set.indicator_self_add_compl s f]
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ μ[Set.indicator s f|m] =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
refine' (this.trans _).symm
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator s f|m]
[PROOFSTEP]
calc
  s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) =ᵐ[μ] s.indicator (μ[s.indicator f|m] + μ[sᶜ.indicator f|m]) :=
    by
    have : μ[s.indicator f + sᶜ.indicator f|m] =ᵐ[μ] μ[s.indicator f|m] + μ[sᶜ.indicator f|m] :=
      condexp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl))
    filter_upwards [this] with x hx
    classical rw [Set.indicator_apply, Set.indicator_apply, hx]
  _ = s.indicator (μ[s.indicator f|m]) + s.indicator (μ[sᶜ.indicator f|m]) := (s.indicator_add' _ _)
  _ =ᵐ[μ] s.indicator (μ[s.indicator f|m]) + s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) :=
    by
    refine' Filter.EventuallyEq.rfl.add _
    have : sᶜ.indicator (μ[sᶜ.indicator f|m]) =ᵐ[μ] μ[sᶜ.indicator f|m] :=
      by
      refine' (condexp_indicator_aux hs.compl _).symm.trans _
      · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
      · rw [Set.indicator_indicator, Set.inter_self]
    filter_upwards [this] with x hx
    by_cases hxs : x ∈ s
    · simp only [hx, hxs, Set.indicator_of_mem]
    · simp only [hxs, Set.indicator_of_not_mem, not_false_iff]
  _ =ᵐ[μ] s.indicator (μ[s.indicator f|m]) := by
    rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
  _ =ᵐ[μ] μ[s.indicator f|m] := by
    refine' (condexp_indicator_aux hs _).symm.trans _
    · exact indicator_ae_eq_restrict_compl (hm _ hs)
    · rw [Set.indicator_indicator, Set.inter_self]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m]) =ᵐ[μ]
    Set.indicator s (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m])
[PROOFSTEP]
have : μ[s.indicator f + sᶜ.indicator f|m] =ᵐ[μ] μ[s.indicator f|m] + μ[sᶜ.indicator f|m] :=
  condexp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl))
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : μ[Set.indicator s f + Set.indicator sᶜ f|m] =ᵐ[μ] μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]
⊢ Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m]) =ᵐ[μ]
    Set.indicator s (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m])
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : μ[Set.indicator s f + Set.indicator sᶜ f|m] =ᵐ[μ] μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]
x : α
hx : (μ[Set.indicator s f + Set.indicator sᶜ f|m]) x = (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]) x
⊢ Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m]) x =
    Set.indicator s (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]) x
[PROOFSTEP]
classical rw [Set.indicator_apply, Set.indicator_apply, hx]
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : μ[Set.indicator s f + Set.indicator sᶜ f|m] =ᵐ[μ] μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]
x : α
hx : (μ[Set.indicator s f + Set.indicator sᶜ f|m]) x = (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]) x
⊢ Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m]) x =
    Set.indicator s (μ[Set.indicator s f|m] + μ[Set.indicator sᶜ f|m]) x
[PROOFSTEP]
rw [Set.indicator_apply, Set.indicator_apply, hx]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s (μ[Set.indicator s f|m]) + Set.indicator s (μ[Set.indicator sᶜ f|m]) =ᵐ[μ]
    Set.indicator s (μ[Set.indicator s f|m]) + Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]))
[PROOFSTEP]
refine' Filter.EventuallyEq.rfl.add _
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ (fun x => Set.indicator s (μ[Set.indicator sᶜ f|m]) x) =ᵐ[μ] fun x =>
    Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) x
[PROOFSTEP]
have : sᶜ.indicator (μ[sᶜ.indicator f|m]) =ᵐ[μ] μ[sᶜ.indicator f|m] :=
  by
  refine' (condexp_indicator_aux hs.compl _).symm.trans _
  · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
  · rw [Set.indicator_indicator, Set.inter_self]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator sᶜ f|m]
[PROOFSTEP]
refine' (condexp_indicator_aux hs.compl _).symm.trans _
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator sᶜ f =ᵐ[Measure.restrict μ sᶜᶜ] 0
[PROOFSTEP]
exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ μ[Set.indicator sᶜ (Set.indicator sᶜ f)|m] =ᵐ[μ] μ[Set.indicator sᶜ f|m]
[PROOFSTEP]
rw [Set.indicator_indicator, Set.inter_self]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator sᶜ f|m]
⊢ (fun x => Set.indicator s (μ[Set.indicator sᶜ f|m]) x) =ᵐ[μ] fun x =>
    Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) x
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator sᶜ f|m]
x : α
hx : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) x = (μ[Set.indicator sᶜ f|m]) x
⊢ Set.indicator s (μ[Set.indicator sᶜ f|m]) x = Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) x
[PROOFSTEP]
by_cases hxs : x ∈ s
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator sᶜ f|m]
x : α
hx : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) x = (μ[Set.indicator sᶜ f|m]) x
hxs : x ∈ s
⊢ Set.indicator s (μ[Set.indicator sᶜ f|m]) x = Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) x
[PROOFSTEP]
simp only [hx, hxs, Set.indicator_of_mem]
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (Measure.trim μ hm)
this✝ : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
this : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) =ᵐ[μ] μ[Set.indicator sᶜ f|m]
x : α
hx : Set.indicator sᶜ (μ[Set.indicator sᶜ f|m]) x = (μ[Set.indicator sᶜ f|m]) x
hxs : ¬x ∈ s
⊢ Set.indicator s (μ[Set.indicator sᶜ f|m]) x = Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) x
[PROOFSTEP]
simp only [hxs, Set.indicator_of_not_mem, not_false_iff]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s (μ[Set.indicator s f|m]) + Set.indicator s (Set.indicator sᶜ (μ[Set.indicator sᶜ f|m])) =ᵐ[μ]
    Set.indicator s (μ[Set.indicator s f|m])
[PROOFSTEP]
rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s (μ[Set.indicator s f|m]) =ᵐ[μ] μ[Set.indicator s f|m]
[PROOFSTEP]
refine' (condexp_indicator_aux hs _).symm.trans _
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ Set.indicator s f =ᵐ[Measure.restrict μ sᶜ] 0
[PROOFSTEP]
exact indicator_ae_eq_restrict_compl (hm _ hs)
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
this : Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[Set.indicator s f + Set.indicator sᶜ f|m])
⊢ μ[Set.indicator s (Set.indicator s f)|m] =ᵐ[μ] μ[Set.indicator s f|m]
[PROOFSTEP]
rw [Set.indicator_indicator, Set.inter_self]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
⊢ Measure.restrict μ s[f|m] =ᵐ[Measure.restrict μ s] μ[f|m]
[PROOFSTEP]
have : SigmaFinite ((μ.restrict s).trim hm) := by rw [← restrict_trim hm _ hs_m]; infer_instance
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
⊢ SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
[PROOFSTEP]
rw [← restrict_trim hm _ hs_m]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
⊢ SigmaFinite (Measure.restrict (Measure.trim μ hm) s)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ Measure.restrict μ s[f|m] =ᵐ[Measure.restrict μ s] μ[f|m]
[PROOFSTEP]
rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ Set.indicator s (Measure.restrict μ s[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m])
[PROOFSTEP]
refine' EventuallyEq.trans _ (condexp_indicator hf_int hs_m)
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ Set.indicator s (Measure.restrict μ s[f|m]) =ᵐ[μ] μ[Set.indicator s f|m]
[PROOFSTEP]
refine' ae_eq_condexp_of_forall_set_integral_eq hm (hf_int.indicator (hm _ hs_m)) _ _ _
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑μ s_1 < ⊤ → IntegrableOn (Set.indicator s (Measure.restrict μ s[f|m])) s_1
[PROOFSTEP]
intro t ht _
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ IntegrableOn (Set.indicator s (Measure.restrict μ s[f|m])) t
[PROOFSTEP]
rw [← integrable_indicator_iff (hm _ ht), Set.indicator_indicator, Set.inter_comm, ← Set.indicator_indicator]
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ Integrable (Set.indicator s (Set.indicator t (Measure.restrict μ s[f|m])))
[PROOFSTEP]
suffices h_int_restrict : Integrable (t.indicator ((μ.restrict s)[f|m])) (μ.restrict s)
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
h_int_restrict : Integrable (Set.indicator t (Measure.restrict μ s[f|m]))
⊢ Integrable (Set.indicator s (Set.indicator t (Measure.restrict μ s[f|m])))
[PROOFSTEP]
rw [integrable_indicator_iff (hm _ hs_m), IntegrableOn]
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
h_int_restrict : Integrable (Set.indicator t (Measure.restrict μ s[f|m]))
⊢ Integrable (Set.indicator t (Measure.restrict μ s[f|m]))
[PROOFSTEP]
rw [integrable_indicator_iff (hm _ ht), IntegrableOn] at h_int_restrict ⊢
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
h_int_restrict : Integrable (Measure.restrict μ s[f|m])
⊢ Integrable (Measure.restrict μ s[f|m])
[PROOFSTEP]
exact h_int_restrict
[GOAL]
case h_int_restrict
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ Integrable (Set.indicator t (Measure.restrict μ s[f|m]))
[PROOFSTEP]
exact integrable_condexp.indicator (hm _ ht)
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ →
        ∫ (x : α) in s_1, Set.indicator s (Measure.restrict μ s[f|m]) x ∂μ = ∫ (x : α) in s_1, Set.indicator s f x ∂μ
[PROOFSTEP]
intro t ht _
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, Set.indicator s (Measure.restrict μ s[f|m]) x ∂μ = ∫ (x : α) in t, Set.indicator s f x ∂μ
[PROOFSTEP]
calc
  ∫ x in t, s.indicator ((μ.restrict s)[f|m]) x ∂μ = ∫ x in t, ((μ.restrict s)[f|m]) x ∂μ.restrict s := by
    rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
      Set.inter_comm]
  _ = ∫ x in t, f x ∂μ.restrict s := (set_integral_condexp hm hf_int.integrableOn ht)
  _ = ∫ x in t, s.indicator f x ∂μ := by
    rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
      Set.inter_comm]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, Set.indicator s (Measure.restrict μ s[f|m]) x ∂μ =
    ∫ (x : α) in t, (Measure.restrict μ s[f|m]) x ∂Measure.restrict μ s
[PROOFSTEP]
rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
  Set.inter_comm]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, f x ∂Measure.restrict μ s = ∫ (x : α) in t, Set.indicator s f x ∂μ
[PROOFSTEP]
rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
  Set.inter_comm]
[GOAL]
case refine'_3
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
hs_m : MeasurableSet s
hf_int : Integrable f
this : SigmaFinite (Measure.trim (Measure.restrict μ s) hm)
⊢ AEStronglyMeasurable' m (Set.indicator s (Measure.restrict μ s[f|m])) μ
[PROOFSTEP]
exact (stronglyMeasurable_condexp.indicator hs_m).aeStronglyMeasurable'
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ μ[f|m] =ᵐ[Measure.restrict μ s] μ[f|m₂]
[PROOFSTEP]
rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
[PROOFSTEP]
have hs_m₂ : MeasurableSet[m₂] s := by rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ MeasurableSet s
[PROOFSTEP]
rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
[PROOFSTEP]
by_cases hf_int : Integrable f μ
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
[PROOFSTEP]
simp_rw [condexp_undef hf_int]
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f
⊢ Set.indicator s 0 =ᵐ[μ] Set.indicator s 0
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ Set.indicator s (μ[f|m]) =ᵐ[μ] Set.indicator s (μ[f|m₂])
[PROOFSTEP]
refine' ((condexp_indicator hf_int hs_m).symm.trans _).trans (condexp_indicator hf_int hs_m₂)
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ μ[Set.indicator s f|m] =ᵐ[μ] μ[Set.indicator s f|m₂]
[PROOFSTEP]
refine'
  ae_eq_of_forall_set_integral_eq_of_sigmaFinite' hm₂ (fun s _ _ => integrable_condexp.integrableOn)
    (fun s _ _ => integrable_condexp.integrableOn) _ _ stronglyMeasurable_condexp.aeStronglyMeasurable'
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ → ∫ (x : α) in s_1, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in s_1, (μ[Set.indicator s f|m₂]) x ∂μ
case pos.refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ AEStronglyMeasurable' m₂ (μ[Set.indicator s f|m]) μ
[PROOFSTEP]
swap
[GOAL]
case pos.refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ AEStronglyMeasurable' m₂ (μ[Set.indicator s f|m]) μ
[PROOFSTEP]
have : StronglyMeasurable[m] (μ[s.indicator f|m]) := stronglyMeasurable_condexp
[GOAL]
case pos.refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
this : StronglyMeasurable (μ[Set.indicator s f|m])
⊢ AEStronglyMeasurable' m₂ (μ[Set.indicator s f|m]) μ
[PROOFSTEP]
refine' this.aeStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) _
[GOAL]
case pos.refine'_2
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
this : StronglyMeasurable (μ[Set.indicator s f|m])
⊢ μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
[PROOFSTEP]
exact condexp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ → ∫ (x : α) in s_1, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in s_1, (μ[Set.indicator s f|m₂]) x ∂μ
[PROOFSTEP]
intro t ht _
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in t, (μ[Set.indicator s f|m₂]) x ∂μ
[PROOFSTEP]
have : ∫ x in t, (μ[s.indicator f|m]) x ∂μ = ∫ x in s ∩ t, (μ[s.indicator f|m]) x ∂μ :=
  by
  rw [← integral_add_compl (hm _ hs_m) integrable_condexp.integrableOn]
  suffices ∫ x in sᶜ, (μ[s.indicator f|m]) x ∂μ.restrict t = 0 by
    rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
  rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
  suffices μ[s.indicator f|m] =ᵐ[μ.restrict sᶜ] 0
    by
    rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
    calc
      ∫ x : α in t, (μ[s.indicator f|m]) x ∂μ.restrict sᶜ = ∫ x : α in t, 0 ∂μ.restrict sᶜ :=
        by
        refine' set_integral_congr_ae (hm₂ _ ht) _
        filter_upwards [this] with x hx _ using hx
      _ = 0 := integral_zero _ _
  refine' condexp_ae_eq_restrict_zero hs_m.compl _
  exact indicator_ae_eq_restrict_compl (hm _ hs_m)
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in s ∩ t, (μ[Set.indicator s f|m]) x ∂μ
[PROOFSTEP]
rw [← integral_add_compl (hm _ hs_m) integrable_condexp.integrableOn]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in s, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t +
      ∫ (x : α) in sᶜ, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t =
    ∫ (x : α) in s ∩ t, (μ[Set.indicator s f|m]) x ∂μ
[PROOFSTEP]
suffices ∫ x in sᶜ, (μ[s.indicator f|m]) x ∂μ.restrict t = 0 by
  rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : ∫ (x : α) in sᶜ, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t = 0
⊢ ∫ (x : α) in s, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t +
      ∫ (x : α) in sᶜ, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t =
    ∫ (x : α) in s ∩ t, (μ[Set.indicator s f|m]) x ∂μ
[PROOFSTEP]
rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in sᶜ, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ t = 0
[PROOFSTEP]
rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in sᶜ ∩ t, (μ[Set.indicator s f|m]) x ∂μ = 0
[PROOFSTEP]
suffices μ[s.indicator f|m] =ᵐ[μ.restrict sᶜ] 0
  by
  rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
  calc
    ∫ x : α in t, (μ[s.indicator f|m]) x ∂μ.restrict sᶜ = ∫ x : α in t, 0 ∂μ.restrict sᶜ :=
      by
      refine' set_integral_congr_ae (hm₂ _ ht) _
      filter_upwards [this] with x hx _ using hx
    _ = 0 := integral_zero _ _
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
⊢ ∫ (x : α) in sᶜ ∩ t, (μ[Set.indicator s f|m]) x ∂μ = 0
[PROOFSTEP]
rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ sᶜ = 0
[PROOFSTEP]
calc
  ∫ x : α in t, (μ[s.indicator f|m]) x ∂μ.restrict sᶜ = ∫ x : α in t, 0 ∂μ.restrict sᶜ :=
    by
    refine' set_integral_congr_ae (hm₂ _ ht) _
    filter_upwards [this] with x hx _ using hx
  _ = 0 := integral_zero _ _
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂Measure.restrict μ sᶜ = ∫ (x : α) in t, 0 ∂Measure.restrict μ sᶜ
[PROOFSTEP]
refine' set_integral_congr_ae (hm₂ _ ht) _
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ sᶜ, x ∈ t → (μ[Set.indicator s f|m]) x = 0
[PROOFSTEP]
filter_upwards [this] with x hx _ using hx
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ μ[Set.indicator s f|m] =ᵐ[Measure.restrict μ sᶜ] 0
[PROOFSTEP]
refine' condexp_ae_eq_restrict_zero hs_m.compl _
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ Set.indicator s f =ᵐ[Measure.restrict μ sᶜ] 0
[PROOFSTEP]
exact indicator_ae_eq_restrict_compl (hm _ hs_m)
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in s ∩ t, (μ[Set.indicator s f|m]) x ∂μ
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in t, (μ[Set.indicator s f|m₂]) x ∂μ
[PROOFSTEP]
have hst_m : MeasurableSet[m] (s ∩ t) := (hs _).mpr (hs_m₂.inter ht)
[GOAL]
case pos.refine'_1
α : Type u_1
𝕜 : Type u_2
E : Type u_3
m✝ m0✝ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ✝ : Measure α
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (Measure.trim μ hm)
inst✝ : SigmaFinite (Measure.trim μ hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
this : ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in s ∩ t, (μ[Set.indicator s f|m]) x ∂μ
hst_m : MeasurableSet (s ∩ t)
⊢ ∫ (x : α) in t, (μ[Set.indicator s f|m]) x ∂μ = ∫ (x : α) in t, (μ[Set.indicator s f|m₂]) x ∂μ
[PROOFSTEP]
simp_rw [this, set_integral_condexp hm₂ (hf_int.indicator (hm _ hs_m)) ht,
  set_integral_condexp hm (hf_int.indicator (hm _ hs_m)) hst_m, integral_indicator (hm _ hs_m),
  Measure.restrict_restrict (hm _ hs_m), ← Set.inter_assoc, Set.inter_self]