[GOAL]
α : Type ?u.37
β : Type ?u.40
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
⊢ inst✝¹ ≤ OuterMeasure.caratheodory (OuterMeasure.dirac a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
⊢ ↑↑(dirac a) s = 1
[PROOFSTEP]
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s = 1
[PROOFSTEP]
refine' le_antisymm (this univ trivial ▸ _) (this s h ▸ le_dirac_apply)
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ indicator univ 1 a
[PROOFSTEP]
rw [← dirac_apply' a MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ ↑↑(dirac a) univ
[PROOFSTEP]
exact measure_mono (subset_univ s)
[GOAL]
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
[GOAL]
case neg
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
rw [indicator_of_not_mem h, ← nonpos_iff_eq_zero]
[GOAL]
case neg
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s ≤ 0
[PROOFSTEP]
calc
  dirac a s ≤ dirac a { a }ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
  _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
[GOAL]
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) {a}ᶜ = 0
[PROOFSTEP]
simp [dirac_apply' _ (measurableSet_singleton _).compl]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f (dirac a)) s = ↑↑(dirac (f a)) s
[PROOFSTEP]
simp [hs, map_apply hf hs, hf hs, indicator_apply]
[GOAL]
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
a : α
⊢ restrict μ {a} = ↑↑μ {a} • dirac a
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
have : s ∩ { a } = { a } := by simpa
[GOAL]
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}
[PROOFSTEP]
simpa
[GOAL]
case pos
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
have : s ∩ { a } = ∅ := inter_singleton_eq_empty.2 ha
[GOAL]
case neg
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
this : s ∩ {a} = ∅
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
[PROOFSTEP]
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' { y }) := fun y _ => hf (measurableSet_singleton _)
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
this : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
[PROOFSTEP]
simp [← tsum_measure_preimage_singleton (to_countable s) this, *, tsum_subtype s fun b => μ (f ⁻¹' { b }), ←
  indicator_mul_right s fun b => μ (f ⁻¹' { b })]
[GOAL]
α : Type u_1
β : Type ?u.17308
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun a => ↑↑μ {a} • dirac a) = μ
[PROOFSTEP]
simpa using (map_eq_sum μ id measurable_id).symm
[GOAL]
α : Type u_1
β : Type ?u.19567
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), indicator s (fun x => ↑↑μ {x}) x = ↑↑(sum fun a => ↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, Set.indicator_apply, mul_ite,
  Pi.one_apply, mul_one, mul_zero]
[GOAL]
α : Type u_1
β : Type ?u.19567
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum fun a => ↑↑μ {a} • dirac a) s = ↑↑μ s
[PROOFSTEP]
rw [μ.sum_smul_dirac]
[GOAL]
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
h : a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]
[GOAL]
case neg
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
h : ¬a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]
[GOAL]
α : Type u_1
β : Type ?u.24298
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type ?u.24298
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a
[PROOFSTEP]
simp [mem_ae_iff, imp_false]
[GOAL]
α : Type u_2
β : Type ?u.26464
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
δ : Type u_1
inst✝ : MeasurableSingletonClass α
a : α
f : α → δ
⊢ f =ᶠ[ae (dirac a)] const α (f a)
[PROOFSTEP]
simp [Filter.EventuallyEq]
[GOAL]
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ Measure.restrict (dirac a) s = if a ∈ s then dirac a else 0
[PROOFSTEP]
split_ifs with has
[GOAL]
case pos
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ Measure.restrict (dirac a) s = dirac a
[PROOFSTEP]
apply restrict_eq_self_of_ae_mem
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
[PROOFSTEP]
rw [ae_dirac_iff]
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ a ∈ s
[PROOFSTEP]
assumption
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ MeasurableSet {x | x ∈ s}
[PROOFSTEP]
assumption
[GOAL]
case neg
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : ¬a ∈ s
⊢ Measure.restrict (dirac a) s = 0
[PROOFSTEP]
rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_not_mem has]
[GOAL]
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ Measure.restrict (dirac a) s = if a ∈ s then dirac a else 0
[PROOFSTEP]
split_ifs with has
[GOAL]
case pos
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ Measure.restrict (dirac a) s = dirac a
[PROOFSTEP]
apply restrict_eq_self_of_ae_mem
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
[PROOFSTEP]
rwa [ae_dirac_eq]
[GOAL]
case neg
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : ¬a ∈ s
⊢ Measure.restrict (dirac a) s = 0
[PROOFSTEP]
rw [restrict_eq_zero, dirac_apply, indicator_of_not_mem has]
