noncomputable def juxt {S : Type u_1} {E : Type u_2} (Λ : Set S) (η : S → E) (ζ : ↑Λ → E) (x : S) : E

Equations

• juxt Λ η ζ x = if h : x ∈ Λ then ζ ⟨x, h⟩ else η x

@[simp]

theorem juxt_apply_of_mem {S : Type u_1} {E : Type u_2} {Λ : Set S} {η : S → E} {x : S} (hx : x ∈ Λ) (ζ : ↑Λ → E) : juxt Λ η ζ x = ζ ⟨x, hx⟩

@[simp]

theorem juxt_apply_of_not_mem {S : Type u_1} {E : Type u_2} {Λ : Set S} {η : S → E} {x : S} (h : x ∉ Λ) (ζ : ↑Λ → E) : juxt Λ η ζ x = η x

theorem Measurable.juxt {S : Type u_1} {E : Type u_2} {𝓔 : MeasurableSpace E} {Λ : Set S} {η : S → E} : Measurable (juxt Λ η)

theorem preimage_juxt_pi {S : Type u_1} {E : Type u_2} {Λ s : Set S} {t : S → Set E} {η : S → E} [DecidablePred fun (x : S) => x ∈ s] (hη : η ∈ (s \ Λ).pi t) : juxt Λ η ⁻¹' s.pi t = Set.univ.pi fun (j : ↑Λ) => if ↑j ∈ s then t ↑j else Set.univ

theorem preimage_juxt_pi_eq_empty {S : Type u_1} {E : Type u_2} {Λ s : Set S} {t : S → Set E} {η : S → E} (hη : η ∉ (s \ Λ).pi t) : juxt Λ η ⁻¹' s.pi t = ∅

theorem map_juxt_pi {S : Type u_1} {E : Type u_2} {𝓔 : MeasurableSpace E} {Λ s : Set S} {t : S → Set E} [DecidablePred fun (x : S) => x ∈ s] (μ : MeasureTheory.Measure (↑Λ → E)) (ht : ∀ (i : S), MeasurableSet (t i)) (hs : s.Countable) (η : S → E) : (MeasureTheory.Measure.map (juxt Λ η) μ) (s.pi t) = ((s \ Λ).pi t).indicator (fun (x : S → E) => μ (Set.univ.pi fun (j : ↑Λ) => if ↑j ∈ s then t ↑j else Set.univ)) η

theorem measurable_map_juxt_pi {S : Type u_1} {E : Type u_2} {𝓔 : MeasurableSpace E} {Λ s : Set S} {t : S → Set E} (μ : MeasureTheory.Measure (↑Λ → E)) (ht : ∀ (i : S), MeasurableSet (t i)) (hs : s.Countable) : Measurable fun (η : S → E) => (MeasureTheory.Measure.map (juxt Λ η) μ) (s.pi t)