feat(measure_theory/integral/bochner): generalize the Bochner integra…

…l construction (#8939)

The construction of the Bochner integral is generalized to a process extending a set function `T : set α → (E →L[ℝ] F)` from sets to functions in L1. The integral corresponds to `T s` equal to the linear map `E →L[ℝ] E` with value `λ x, (μ s).to_real • x`.

The conditional expectation from L1 to L1 will be defined by taking for `T` the function `condexp_ind : set α → (E →L[ℝ] α →₁[μ] E)` defined in #8920 .

src/algebra/pointwise.lean

@@ -406,6 +406,9 @@ by { rw [← inv_subset_inv, set.inv_inv] }
 @[to_additive] lemma finite.inv [group α] {s : set α} (hs : finite s) : finite s⁻¹ :=
 hs.preimage $ inv_injective.inj_on _
 
+@[to_additive] lemma inv_singleton {β : Type*} [group β] (x : β) : ({x} : set β)⁻¹ = {x⁻¹} :=
+by { ext1 y, rw [mem_inv, mem_singleton_iff, mem_singleton_iff, inv_eq_iff_inv_eq, eq_comm], }
+
 /-! ### Properties about scalar multiplication -/
 
 /-- The scaling of a set `(x • s : set β)` by a scalar `x ∶ α` is defined as `{x • y | y ∈ s}`

src/measure_theory/function/l1_space.lean

@@ -857,7 +857,10 @@ variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] [measurable_
   [opens_measurable_space 𝕜]
 
 lemma to_L1_smul (f : α → β) (hf : integrable f μ) (k : 𝕜) :
-  to_L1 (λa, k • f a) (hf.smul k) = k • to_L1 f hf := rfl
+  to_L1 (λ a, k • f a) (hf.smul k) = k • to_L1 f hf := rfl
+
+lemma to_L1_smul' (f : α → β) (hf : integrable f μ) (k : 𝕜) :
+  to_L1 (k • f) (hf.smul k) = k • to_L1 f hf := rfl
 
 end integrable