1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68

import analysis.normed_space.finite_dimension
import analysis.convolution
import measure_theory.function.jacobian
import measure_theory.integral.bochner
import measure_theory.measure.lebesgue

open set filter
open_locale topological_space filter ennreal
open measure_theory

noncomputable theory

variables {α : Type*} [measurable_space α]
variables {μ : measure α}

section

variables {E : Type*} [normed_group E] [normed_space ℝ E] [complete_space E]
  {f : α → E}

example {f g : α → E} (hf : integrable f μ) (hg : integrable g μ) :
  ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
integral_add hf hg

example {s : set α} (c : E) :
  ∫ x in s, c ∂μ = (μ s).to_real • c :=
set_integral_const c

example {F : ℕ → α → E} {f : α → E} (bound : α → ℝ)
  (hmeas : ∀ n, ae_strongly_measurable (F n) μ)
  (hint : integrable bound μ)
  (hbound : ∀ n, ∀ᵐ a ∂μ, ∥F n a∥ ≤ bound a)
  (hlim : ∀ᵐ a ∂μ, tendsto (λ (n : ℕ), F n a) at_top (𝓝 (f a))) :
  tendsto (λ n, ∫ a, F n a ∂μ) at_top (𝓝 (∫ a, f a ∂μ)) :=
tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim

example
  {α : Type*} [measurable_space α]
  {μ : measure α} [sigma_finite μ]
  {β : Type*} [measurable_space β] {ν : measure β} [sigma_finite ν]
  (f : α × β → E) (hf : integrable f (μ.prod ν)) :
  ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ :=
integral_prod f hf

end
section
open_locale convolution

variables {𝕜 : Type*} {G : Type*} {E : Type*} {E' : Type*} {F : Type*} [normed_group E]
  [normed_group E'] [normed_group F] [nondiscrete_normed_field 𝕜]
  [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F]
  [measurable_space G] [normed_space ℝ F] [complete_space F] [has_sub G]

example (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : measure G) :
  f ⋆[L, μ] g = λ x, ∫ t, L (f t) (g (x - t)) ∂μ :=
rfl

end
example {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
  [measurable_space E] [borel_space E] (μ : measure E) [μ.is_add_haar_measure]
  {F : Type*}[normed_group F] [normed_space ℝ F] [complete_space F]
  {s : set E} {f : E → E} {f' : E → (E →L[ℝ] E)}
  (hs : measurable_set s)
  (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x)
  (h_inj : inj_on f s)
  (g : E → F) :
  ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ :=
integral_image_eq_integral_abs_det_fderiv_smul μ hs hf h_inj g