-
Notifications
You must be signed in to change notification settings - Fork 259
/
Basic.lean
124 lines (88 loc) · 4.4 KB
/
Basic.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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
/-
Copyright (c) 2023 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.MeasureTheory.Function.AEEqFun.DomAct
import Mathlib.MeasureTheory.Function.LpSpace
/-!
# Action of `Mᵈᵐᵃ` on `Lᵖ` spaces
In this file we define action of `Mᵈᵐᵃ` on `MeasureTheory.Lp E p μ`
If `f : α → E` is a function representing an equivalence class in `Lᵖ(α, E)`, `M` acts on `α`,
and `c : M`, then `(.mk c : Mᵈᵐᵃ) • [f]` is represented by the function `a ↦ f (c • a)`.
We also prove basic properties of this action.
-/
set_option autoImplicit true
open MeasureTheory Filter
open scoped ENNReal
namespace DomMulAct
variable {M N α E : Type*} [MeasurableSpace M] [MeasurableSpace N]
[MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ℝ≥0∞}
section SMul
variable [SMul M α] [SMulInvariantMeasure M α μ] [MeasurableSMul M α]
@[to_additive]
instance : SMul Mᵈᵐᵃ (Lp E p μ) where
smul c f := Lp.compMeasurePreserving (mk.symm c • ·) (measurePreserving_smul _ _) f
@[to_additive (attr := simp)]
theorem smul_Lp_val (c : Mᵈᵐᵃ) (f : Lp E p μ) : (c • f).1 = c • f.1 := rfl
@[to_additive]
theorem smul_Lp_ae_eq (c : Mᵈᵐᵃ) (f : Lp E p μ) : c • f =ᵐ[μ] (f <| mk.symm c • ·) :=
Lp.coeFn_compMeasurePreserving _ _
@[to_additive]
theorem mk_smul_toLp (c : M) {f : α → E} (hf : Memℒp f p μ) :
mk c • hf.toLp f =
(hf.comp_measurePreserving <| measurePreserving_smul c μ).toLp (f <| c • ·) :=
rfl
@[to_additive (attr := simp)]
theorem smul_Lp_const [IsFiniteMeasure μ] (c : Mᵈᵐᵃ) (a : E) :
c • Lp.const p μ a = Lp.const p μ a :=
rfl
instance [SMul N α] [SMulCommClass M N α] [SMulInvariantMeasure N α μ] [MeasurableSMul N α] :
SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (Lp E p μ) :=
Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl
instance [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : SMulCommClass Mᵈᵐᵃ 𝕜 (Lp E p μ) :=
Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl
instance [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : SMulCommClass 𝕜 Mᵈᵐᵃ (Lp E p μ) :=
.symm _ _ _
-- We don't have a typeclass for additive versions of the next few lemmas
-- Should we add `AddDistribAddAction` with `to_additive` both from `MulDistribMulAction`
-- and `DistribMulAction`?
@[to_additive]
theorem smul_Lp_add (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f + g) = c • f + c • g := by
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
attribute [simp] DomAddAct.vadd_Lp_add
@[to_additive (attr := simp 1001)]
theorem smul_Lp_zero (c : Mᵈᵐᵃ) : c • (0 : Lp E p μ) = 0 := rfl
@[to_additive]
theorem smul_Lp_neg (c : Mᵈᵐᵃ) (f : Lp E p μ) : c • (-f) = -(c • f) := by
rcases f with ⟨⟨_⟩, _⟩; rfl
@[to_additive]
theorem smul_Lp_sub (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f - g) = c • f - c • g := by
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
instance : DistribSMul Mᵈᵐᵃ (Lp E p μ) where
smul_zero _ := rfl
smul_add := by rintro _ ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
-- The next few lemmas follow from the `IsometricSMul` instance if `1 ≤ p`
@[to_additive (attr := simp)]
theorem norm_smul_Lp (c : Mᵈᵐᵃ) (f : Lp E p μ) : ‖c • f‖ = ‖f‖ :=
Lp.norm_compMeasurePreserving _ _
@[to_additive (attr := simp)]
theorem nnnorm_smul_Lp (c : Mᵈᵐᵃ) (f : Lp E p μ) : ‖c • f‖₊ = ‖f‖₊ :=
NNReal.eq <| Lp.norm_compMeasurePreserving _ _
@[to_additive (attr := simp)]
theorem dist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : dist (c • f) (c • g) = dist f g := by
simp only [dist, ← smul_Lp_sub, norm_smul_Lp]
@[to_additive (attr := simp)]
theorem edist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : edist (c • f) (c • g) = edist f g := by
simp only [Lp.edist_dist, dist_smul_Lp]
variable [Fact (1 ≤ p)]
instance : IsometricSMul Mᵈᵐᵃ (Lp E p μ) := ⟨edist_smul_Lp⟩
end SMul
section MulAction
variable [Monoid M] [MulAction M α] [SMulInvariantMeasure M α μ] [MeasurableSMul M α]
@[to_additive]
instance : MulAction Mᵈᵐᵃ (Lp E p μ) := Subtype.val_injective.mulAction _ fun _ _ ↦ rfl
instance : DistribMulAction Mᵈᵐᵃ (Lp E p μ) :=
Subtype.val_injective.distribMulAction ⟨⟨_, rfl⟩, fun _ _ ↦ rfl⟩ fun _ _ ↦ rfl
end MulAction
end DomMulAct