-
Notifications
You must be signed in to change notification settings - Fork 259
/
Inner.lean
60 lines (50 loc) · 2.57 KB
/
Inner.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
/-!
# Measurability of scalar products
-/
variable {α : Type*} {𝕜 : Type*} {E : Type*}
variable [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
@[aesop safe 20 apply (rule_sets := [Measurable])]
theorem Measurable.inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
[SecondCountableTopology E] {f g : α → E} (hf : Measurable f)
(hg : Measurable g) : Measurable fun t => ⟪f t, g t⟫ :=
Continuous.measurable2 continuous_inner hf hg
@[measurability]
theorem Measurable.const_inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
[SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
Measurable fun t => ⟪c, f t⟫ :=
Measurable.inner measurable_const hf
@[measurability]
theorem Measurable.inner_const {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
[SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
Measurable fun t => ⟪f t, c⟫ :=
Measurable.inner hf measurable_const
@[aesop safe 20 apply (rule_sets := [Measurable])]
theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
[SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun x => ⟪f x, g x⟫) μ := by
refine ⟨fun x => ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, ?_⟩
refine hf.ae_eq_mk.mp (hg.ae_eq_mk.mono fun x hxg hxf => ?_)
dsimp only
congr
set_option linter.unusedVariables false in
@[measurability]
theorem AEMeasurable.const_inner {m : MeasurableSpace α} [MeasurableSpace E]
[OpensMeasurableSpace E] [SecondCountableTopology E]
{μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
AEMeasurable (fun x => ⟪c, f x⟫) μ :=
AEMeasurable.inner aemeasurable_const hf
set_option linter.unusedVariables false in
@[measurability]
theorem AEMeasurable.inner_const {m : MeasurableSpace α} [MeasurableSpace E]
[OpensMeasurableSpace E] [SecondCountableTopology E]
{μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
AEMeasurable (fun x => ⟪f x, c⟫) μ :=
AEMeasurable.inner hf aemeasurable_const