def MeasureTheory.essProjFst {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} (s : Set (α × β)) (ν : Measure β) : Set α

For a (s : Set (α × β)) and (ν : Measure β), we define essProjFst such that x ∈ essProjFst s ν iff 0 < ν {y | ⟨x, y⟩ ∈ s}.

Equations

• MeasureTheory.essProjFst s ν = {x : α | 0 < ν ((fun (x_1 : β) => (x, x_1)) ⁻¹' s)}

def MeasureTheory.essProjSnd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} (s : Set (α × β)) (μ : Measure α) : Set β

For a (s : Set (α × β)) and (μ : Measure α), we define essProjSnd such that y ∈ essProjSnd s μ iff 0 < μ {x | ⟨x, y⟩ ∈ s}.

Equations

• MeasureTheory.essProjSnd s μ = {y : β | 0 < μ ((fun (x : α) => (x, y)) ⁻¹' s)}

theorem MeasureTheory.essProjSnd_eq_essProjFst_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set (α × β)} : essProjSnd s μ = essProjFst (Prod.swap ⁻¹' s) μ

theorem MeasureTheory.essProjFst_subset {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s : Set (α × β)} : essProjFst s ν ⊆ Prod.fst '' s

theorem MeasureTheory.essProjSnd_subset {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set (α × β)} : essProjSnd s μ ⊆ Prod.snd '' s

theorem MeasureTheory.essProjFst_eq {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s : Set (α × β)} : essProjFst s ν = (fun (x : α) => ν ((fun (y : β) => (x, y)) ⁻¹' s)) ⁻¹' Set.Ioi 0

theorem MeasureTheory.essProjSnd_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set (α × β)} : essProjSnd s μ = (fun (y : β) => μ ((fun (x : α) => (x, y)) ⁻¹' s)) ⁻¹' Set.Ioi 0

theorem MeasureTheory.essProjFst_eq' {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s : Set (α × β)} : essProjFst s ν = Function.support fun (x : α) => ν ((fun (y : β) => (x, y)) ⁻¹' s)

theorem MeasureTheory.essProjSnd_eq' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set (α × β)} : essProjSnd s μ = Function.support fun (y : β) => μ ((fun (x : α) => (x, y)) ⁻¹' s)

@[simp]

theorem MeasureTheory.essProjFst_times_univ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s : Set α} (h : ν ≠ 0) : essProjFst (s ×ˢ Set.univ) ν = s

@[simp]

theorem MeasureTheory.essProjSnd_univ_times {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set β} (h : μ ≠ 0) : essProjSnd (Set.univ ×ˢ s) μ = s

theorem MeasureTheory.essProjFst_mono {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s t : Set (α × β)} (h : s ⊆ t) : essProjFst s ν ⊆ essProjFst t ν

theorem MeasureTheory.essProjSnd_mono {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s t : Set (α × β)} (h : s ⊆ t) : essProjSnd s μ ⊆ essProjSnd t μ

theorem MeasureTheory.essProjFst_inter_times_univ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} {s : Set (α × β)} {t : Set α} : essProjFst (s ∩ t ×ˢ Set.univ) ν = essProjFst s ν ∩ t

theorem MeasureTheory.essProjSnd_inter_univ_times {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {s : Set (α × β)} {t : Set β} : essProjSnd (s ∩ Set.univ ×ˢ t) μ = essProjSnd s μ ∩ t

theorem MeasureTheory.measurableSet_essProjFst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) : MeasurableSet (essProjFst s ν)

theorem MeasureTheory.measurableSet_essProjSnd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ] {s : Set (α × β)} (hs : MeasurableSet s) : MeasurableSet (essProjSnd s μ)

theorem MeasureTheory.measure_essProjFst_pos_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) : 0 < μ (essProjFst s ν) ↔ 0 < (μ.prod ν) s

theorem MeasureTheory.measure_essProjSnd_pos_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) : 0 < ν (essProjSnd s μ) ↔ 0 < (μ.prod ν) s

theorem MeasureTheory.exists_subset_measure_fst_image_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SigmaFinite μ] [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h : 0 < (μ.prod ν) s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < (μ.prod ν) t ∧ μ (Prod.fst '' t) < ⊤

theorem MeasureTheory.exists_subset_measure_snd_image_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SigmaFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h : 0 < (μ.prod ν) s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < (μ.prod ν) t ∧ ν (Prod.snd '' t) < ⊤

theorem MeasureTheory.exists_subset_measure_essProjFst_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [NoAtoms' μ] [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h : 0 < (μ.prod ν) s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < (μ.prod ν) t ∧ μ (essProjFst t ν) < μ (essProjFst s ν)

theorem MeasureTheory.exists_subset_measure_essProjSnd_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] [NoAtoms' ν] {s : Set (α × β)} (hs : MeasurableSet s) (h : 0 < (μ.prod ν) s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < (μ.prod ν) t ∧ ν (essProjSnd t μ) < ν (essProjSnd s μ)

theorem MeasureTheory.setLIntegral_strict_mono_set {α : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {s t : Set α} (hf : Measurable f) (hsm : MeasurableSet s) (htm : MeasurableSet t) (htsf : t \ s ⊆ Function.support f) (hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) (hst : s ⊆ t) (h : μ s < μ t) : ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in t, f x ∂μ

instance MeasureTheory.prod.instNoAtoms_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [NoAtoms' μ] [SFinite μ] [SigmaFinite ν] : NoAtoms' (μ.prod ν)

theorem MeasureTheory.isAtom_swap_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] {s : Set (α × β)} : IsAtom (Prod.swap ⁻¹' s) (ν.prod μ) ↔ IsAtom s (μ.prod ν)

instance MeasureTheory.prod.instNoAtoms_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SigmaFinite μ] [NoAtoms' ν] [SFinite ν] : NoAtoms' (μ.prod ν)