diff --git a/scripts/nolints.txt b/scripts/nolints.txt index c8d4815c37ada..be8da310f1962 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -2671,6 +2671,7 @@ side side.other side.to_string simp_attr.functor_norm +simp_attr.integral_simps simp_attr.monad_norm simp_attr.parity_simps simp_attr.push_cast diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index 2850991376ccc..541be3df1fe60 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/src/analysis/normed_space/operator_norm.lean @@ -363,7 +363,7 @@ end section uniformly_extend -variables [complete_space F] {e : E →L[𝕜] G} (h_dense : dense_range e) +variables [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e) section variables (h_e : uniform_inducing e) @@ -393,7 +393,7 @@ have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous, cont := cont } -@[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) h_dense h_e = 0 := +@[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 := begin apply ext, refine is_closed_property h_dense (is_closed_eq _ _) _, @@ -407,7 +407,7 @@ end section variables {N : ℝ} (h_e : ∀x, ∥x∥ ≤ N * ∥e x∥) -local notation `ψ` := f.extend h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing +local notation `ψ` := f.extend e h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the norm of the extension of `f` along `e` is bounded by `N * ∥f∥`. -/ diff --git a/src/measure_theory/ae_eq_fun.lean b/src/measure_theory/ae_eq_fun.lean index 2cd30200dea2b..8ba662dd192dc 100644 --- a/src/measure_theory/ae_eq_fun.lean +++ b/src/measure_theory/ae_eq_fun.lean @@ -349,11 +349,11 @@ variables {γ : Type*} [topological_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ] protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) := -λ c f, comp (has_scalar.smul c) (measurable_smul measurable_id) f +λ c f, comp (has_scalar.smul c) (measurable_smul _ measurable_id) f instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩ -@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul hf) := +@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul _ hf) := rfl lemma smul_to_fun (c : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a := diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean index 04747c121504c..8e8c84b82b7a6 100644 --- a/src/measure_theory/bochner_integration.lean +++ b/src/measure_theory/bochner_integration.lean @@ -620,20 +620,20 @@ protected lemma uniform_embedding : uniform_embedding (coe : (α →₁ₛ β) uniform_embedding_comap subtype.val_injective protected lemma uniform_inducing : uniform_inducing (coe : (α →₁ₛ β) → (α →₁ β)) := -l1.simple_func.uniform_embedding.to_uniform_inducing +simple_func.uniform_embedding.to_uniform_inducing protected lemma dense_embedding : dense_embedding (coe : (α →₁ₛ β) → (α →₁ β)) := -l1.simple_func.uniform_embedding.dense_embedding $ +simple_func.uniform_embedding.dense_embedding $ λ f, mem_closure_iff_nhds.2 $ λ t ht, let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in let ⟨s, h⟩ := exists_simple_func_near f ε0 in ne_empty_iff_exists_mem.2 ⟨_, hε (metric.mem_ball'.2 h), s, rfl⟩ protected lemma dense_inducing : dense_inducing (coe : (α →₁ₛ β) → (α →₁ β)) := -l1.simple_func.dense_embedding.to_dense_inducing +simple_func.dense_embedding.to_dense_inducing -protected lemma closure_range : closure (range (coe : (α →₁ₛ β) → (α →₁ β))) = univ := -l1.simple_func.dense_embedding.to_dense_inducing.closure_range +protected lemma dense_range : dense_range (coe : (α →₁ₛ β) → (α →₁ β)) := +simple_func.dense_inducing.dense variables (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 β] @@ -654,7 +654,7 @@ section simple_func_integral variables [normed_space ℝ β] -/-- Bochner integration over simple functions in l1 space. -/ +/-- The Bochner integral over simple functions in l1 space. -/ def integral (f : α →₁ₛ β) : β := simple_func.bintegral (f.to_simple_func) lemma integral_eq_lintegral {f : α →₁ₛ ℝ} (h_pos : ∀ₘ a, 0 ≤ f.to_simple_func a) : @@ -689,7 +689,7 @@ begin exact f.to_simple_func.norm_bintegral_le_bintegral_norm f.integrable end -/-- Bochner integration over simple functions in l1 space as a continuous linear map. -/ +/-- The Bochner integral over simple functions in l1 space as a continuous linear map. -/ def integral_clm : (α →₁ₛ β) →L[ℝ] β := linear_map.with_bound ⟨integral, integral_add, integral_smul⟩ ⟨1, (λf, le_trans (norm_integral_le_norm _) $ by rw one_mul)⟩ @@ -711,6 +711,144 @@ end simple_func_integral end simple_func +open simple_func + +variables [normed_space ℝ β] [normed_space ℝ γ] [complete_space β] + +local notation `to_l1` := coe_to_l1 α β ℝ +local attribute [instance] simple_func.normed_group simple_func.normed_space + +open continuous_linear_map + +/-- The Bochner integral in l1 space as a continuous linear map. -/ +def integral_clm : (α →₁ β) →L[ℝ] β := + integral_clm.extend to_l1 simple_func.dense_range simple_func.uniform_inducing + +/-- The Bochner integral in l1 space -/ +def integral (f : α →₁ β) : β := (integral_clm).to_fun f + +lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := rfl + +variables (α β) +@[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 := +map_zero integral_clm +variables {α β} + +lemma integral_add (f g : α →₁ β) : integral (f + g) = integral f + integral g := +map_add integral_clm f g + +lemma integral_neg (f : α →₁ β) : integral (-f) = - integral f := +map_neg integral_clm f + +lemma integral_sub (f g : α →₁ β) : integral (f - g) = integral f - integral g := +map_sub integral_clm f g + +lemma integral_smul (r : ℝ) (f : α →₁ β) : integral (r • f) = r • integral f := +map_smul r integral_clm f + end l1 +variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [complete_space β] + [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ] + +/-- The Bochner integral -/ +def integral (f : α → β) : β := +if hf : measurable f ∧ integrable f +then (l1.of_fun f hf.1 hf.2).integral +else 0 + +section properties + +open continuous_linear_map measure_theory.simple_func + +variables {f g : α → β} + +lemma integral_eq (f : α → β) : integral f = + if hf : measurable f ∧ integrable f then (l1.of_fun f hf.1 hf.2).integral else 0 := rfl + +lemma integral_eq_zero_of_non_measurable (h : ¬ measurable f) : integral f = 0 := +by { rw [integral, dif_neg], rw not_and_distrib, exact or.inl h } + +lemma integral_eq_zero_of_non_integrable (h : ¬ integrable f) : integral f = 0 := +by { rw [integral, dif_neg], rw not_and_distrib, exact or.inr h } + +variables (α β) +@[simp] lemma integral_zero : integral (0 : α → β) = 0 := +begin + simp only [integral], rw dif_pos, + { apply l1.integral_zero }, + { exact ⟨(measurable_const : measurable (λb:α, (0:β))), integrable_zero⟩ } +end +variables {α β} + +lemma integral_add (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) + (hgi : integrable g) : integral (f + g) = integral f + integral g := +begin + simp only [integral], repeat { rw dif_pos }, + { rw ← l1.integral_add, refl }, + { exact ⟨hgm, hgi⟩ }, + { exact ⟨hfm, hfi⟩ }, + { exact ⟨measurable_add hfm hgm, integrable_add hfm hgm hfi hgi⟩ } +end + +lemma integral_neg (f : α → β) : integral (-f) = - integral f := +begin + simp only [integral], + by_cases hfm : measurable f, by_cases hfi : integrable f, + { repeat { rw dif_pos }, + { rw ← l1.integral_neg, refl }, + { exact ⟨hfm, hfi⟩ }, + { exact ⟨measurable_neg hfm, integrable_neg hfi⟩ } }, + { repeat { rw dif_neg }, + { rw neg_zero }, + { rw not_and_distrib, exact or.inr hfi }, + { rw not_and_distrib, rw integrable_neg_iff, exact or.inr hfi } }, + { repeat { rw dif_neg }, + { rw neg_zero }, + { rw not_and_distrib, exact or.inl hfm }, + { rw not_and_distrib, rw measurable_neg_iff, exact or.inl hfm } } +end + +lemma integral_sub (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) + (hgi : integrable g) : integral (f - g) = integral f - integral g := +begin + simp only [integral], repeat {rw dif_pos}, + { rw ← l1.integral_sub, refl }, + { exact ⟨hgm, hgi⟩ }, + { exact ⟨hfm, hfi⟩ }, + { exact ⟨measurable_sub hfm hgm, integrable_sub hfm hgm hfi hgi⟩ } +end + +lemma integral_smul (r : ℝ) (f : α → β) : integral (λx, r • (f x)) = r • integral f := +begin + by_cases r0 : r = 0, + { have : (λx, r • (f x)) = 0, { funext, rw [r0, zero_smul, pi.zero_apply] }, + rw [this, r0, zero_smul], apply integral_zero }, + simp only [integral], + by_cases hfm : measurable f, by_cases hfi : integrable f, + { rw dif_pos, rw dif_pos, + { rw ← l1.integral_smul, refl }, + { exact ⟨hfm, hfi⟩ }, + { exact ⟨measurable_smul _ hfm, integrable_smul _ hfi⟩ } }, + { repeat { rw dif_neg }, + { rw smul_zero }, + { rw not_and_distrib, exact or.inr hfi }, + { rw not_and_distrib, + have : (λx, r • (f x)) = r • f, { funext, simp only [pi.smul_apply] }, + rw [this, integrable_smul_iff r0], exact or.inr hfi } }, + { repeat { rw dif_neg }, + { rw smul_zero }, + { rw not_and_distrib, exact or.inl hfm }, + { rw not_and_distrib, rw [measurable_smul_iff r0], exact or.inl hfm, apply_instance } }, +end + +end properties + +run_cmd mk_simp_attr `integral_simps + +attribute [integral_simps] integral_neg integral_smul l1.integral_add l1.integral_sub + l1.integral_smul l1.integral_neg + +attribute [irreducible] integral l1.integral + end measure_theory diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean index eed5538dd01a6..05001bc0cc06b 100644 --- a/src/measure_theory/borel_space.lean +++ b/src/measure_theory/borel_space.lean @@ -209,6 +209,19 @@ lemma measurable_neg (hf : measurable f) : measurable (λa, - f a) := (measurable_of_continuous continuous_neg').comp hf +lemma measurable_neg_iff + [add_group α] [topological_add_group α] [measurable_space β] (f : β → α) : + measurable (-f) ↔ measurable f := +iff.intro +begin + assume h, + have := measurable_neg h, + convert this, + funext, + simp only [pi.neg_apply, _root_.neg_neg] +end +$ measurable_neg + lemma measurable_sub [add_group α] [topological_add_group α] [second_countable_topology α] [measurable_space β] {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a - g a) := @@ -506,8 +519,23 @@ lemma measurable_smul {α : Type*} {β : Type*} {γ : Type*} [semiring α] [topological_space α] [topological_space β] [add_comm_monoid β] [semimodule α β] [topological_semimodule α β] [measurable_space γ] - {c : α} {g : γ → β} (hg : measurable g) : measurable (λ x, c • g x) := -measurable.comp (measurable_of_continuous (continuous_smul continuous_const continuous_id)) hg + (c : α) {f : γ → β} (hf : measurable f) : measurable (λ x, c • f x) := +measurable.comp (measurable_of_continuous (continuous_smul continuous_const continuous_id)) hf + +lemma measurable_smul_iff {α : Type*} {β : Type*} {γ : Type*} + [division_ring α] [topological_space α] + [topological_space β] [add_comm_monoid β] + [semimodule α β] [topological_semimodule α β] [measurable_space γ] + {c : α} (hc : c ≠ 0) (f : γ → β) : measurable (λ x, c • f x) ↔ measurable f := +iff.intro +begin + assume h, + have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f, + { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] }, + have := measurable_smul c⁻¹ h, + rwa eq at this +end +$ measurable_smul c lemma measurable_dist' {α : Type*} [metric_space α] [second_countable_topology α] : measurable (λp:α×α, dist p.1 p.2) := diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean index f5896133ccb28..a1679a6de69e6 100644 --- a/src/measure_theory/l1_space.lean +++ b/src/measure_theory/l1_space.lean @@ -142,6 +142,15 @@ lemma integrable_neg {f : α → β} : integrable f → integrable (-f) := assume hfi, calc _ = _ : lintegral_nnnorm_neg ... < ⊤ : hfi +lemma integrable_neg_iff (f : α → β) : integrable (-f) ↔ integrable f := +begin + split, + { assume h, + have := integrable_neg h, + rwa _root_.neg_neg at this }, + exact integrable_neg +end + lemma integrable_sub {f g : α → β} (hf : measurable f) (hg : measurable g) : integrable f → integrable g → integrable (f - g) := λ hfi hgi, @@ -175,6 +184,15 @@ begin end end +lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f := +begin + split, + { assume h, + have := integrable_smul c⁻¹ h, + rwa [smul_smul, inv_mul_cancel hc, one_smul] at this }, + exact integrable_smul _ +end + end normed_space variables [second_countable_topology β] @@ -331,7 +349,7 @@ rfl variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β] lemma of_fun_smul (f : α → β) (hfm hfi) (k : 𝕜) : - of_fun (k • f) (measurable_smul hfm) (integrable_smul _ hfi) = k • of_fun f hfm hfi := rfl + of_fun (k • f) (measurable_smul _ hfm) (integrable_smul _ hfi) = k • of_fun f hfm hfi := rfl end of_fun