MaskPerturbation.lean

1 import Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
2 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
3 import Mathlib.Basic.Complex.Basic
4 import Mathlib.Tactic
5 
6 /-! Author: Komorebi P. Measurable jump-mask perturbations, with extended Lp norms. -/
7 namespace KomorebiPaperV.MaskPerturbation
8 open MeasureTheory
9 open scoped ENNReal symmDiff
10 variable {Ω : Type*} [MeasurableSpace Ω]
11 
12 noncomputable def jump (S : Set Ω) (a : ℂ) : Ω → ℂ := S.indicator (fun _ => a)
13 
14 theorem jump_measurable (S : Set Ω) (hS : MeasurableSet S) (a : ℂ) (μ : Measure Ω) :
15     AEStronglyMeasurable (jump S a) μ :=
16   (stronglyMeasurable_const.indicator hS).aestronglyMeasurable
17 
18 theorem symmetric_difference_norm (μ : Measure Ω) (S T : Set Ω)
19     (hS : MeasurableSet S) (hT : MeasurableSet T) (p : ENNReal)
20     (hp : p ≠ 0) (hpTop : p ≠ ∞) (a : ℂ) :
21     eLpNorm (jump S a-jump T a) p μ = ‖a‖ₑ * μ (S ∆ T) ^ (1 / p.toReal) := by
22   rw [jump, jump, eLpNorm_indicator_sub_indicator]
23   exact eLpNorm_indicator_const (hS.symmDiff hT) hp hpTop
24 
25 theorem indicator_difference_norm (μ : Measure Ω) (S T : Set Ω)
26     (hS : MeasurableSet S) (hT : MeasurableSet T) (p : ENNReal)
27     (hp : p ≠ 0) (hpTop : p ≠ ∞) :
28     eLpNorm (jump S 1-jump T 1) p μ = μ (S ∆ T) ^ (1 / p.toReal) := by
29   simpa using symmetric_difference_norm μ S T hS hT p hp hpTop 1
30 
31 omit [MeasurableSpace Ω] in
32 theorem jump_sub_same_set (S : Set Ω) (a b : ℂ) : jump S a-jump S b = jump S (a-b) := by
33   classical
34   funext x
35   by_cases hx : x ∈ S <;> simp [jump, hx]
36 
37 omit [MeasurableSpace Ω] in
38 theorem jump_error_decomposition (S T : Set Ω) (a b : ℂ) :
39     jump S a-jump T b = jump S (a-b)+(jump S b-jump T b) := by
40   rw [← jump_sub_same_set]
41   abel
42 
43 theorem finite_p_perturbation (μ : Measure Ω) (S T : Set Ω)
44     (hS : MeasurableSet S) (hT : MeasurableSet T) (p : ENNReal)
45     (hp : 1 ≤ p) (hpTop : p ≠ ∞) (a b : ℂ) :
46     eLpNorm (jump S a-jump T b) p μ ≤
47       ‖a-b‖ₑ * μ S ^ (1 / p.toReal) + ‖b‖ₑ * μ (S ∆ T) ^ (1 / p.toReal) := by
48   have hp0 : p ≠ 0 := ne_of_gt (lt_of_lt_of_le (by norm_num) hp)
49   rw [jump_error_decomposition]
50   calc
51     _ ≤ eLpNorm (jump S (a-b)) p μ + eLpNorm (jump S b-jump T b) p μ :=
52       eLpNorm_add_le (jump_measurable S hS (a-b) μ)
53         ((jump_measurable S hS b μ).sub (jump_measurable T hT b μ)) hp
54     _ = _ := by
55       rw [symmetric_difference_norm μ S T hS hT p hp0 hpTop,
56         jump, eLpNorm_indicator_const hS hp0 hpTop]
57 
58 omit [MeasurableSpace Ω] in
59 theorem pointwise_sup_bound (S T : Set Ω) (a b : ℂ) (x : Ω) :
60     ‖(jump S a-jump T b) x‖ ≤ ‖a-b‖ + if S ∆ T = ∅ then 0 else ‖b‖ := by
61   classical
62   rw [jump_error_decomposition]
63   calc
64     _ ≤ ‖jump S (a-b) x‖ + ‖(jump S b-jump T b) x‖ := norm_add_le _ _
65     _ ≤ ‖a-b‖ + if S ∆ T = ∅ then 0 else ‖b‖ := by
66       apply add_le_add
67       · by_cases hx : x ∈ S <;> simp [jump, hx]
68       · by_cases he : S ∆ T = ∅
69         · have hST : S = T := symmDiff_eq_bot.mp he
70           simp [hST]
71         · by_cases hx : x ∈ S <;> by_cases hy : x ∈ T <;> simp [jump, hx, hy, he]
72 
73 theorem infinity_perturbation (μ : Measure Ω) (S T : Set Ω) (a b : ℂ) :
74     eLpNorm (jump S a-jump T b) ∞ μ ≤
75       ENNReal.ofReal (‖a-b‖ + if S ∆ T = ∅ then 0 else ‖b‖) := by
76   rw [eLpNorm_exponent_top]
77   exact eLpNormEssSup_le_of_ae_bound (ae_of_all μ (pointwise_sup_bound S T a b))
78 
79 theorem full_signal_perturbation (μ : Measure Ω) (S T : Set Ω)
80     (hS : MeasurableSet S) (hT : MeasurableSet T) (p : ENNReal)
81     (hp : 1 ≤ p) (hpTop : p ≠ ∞) (a b : ℂ) (s t : Ω → ℂ)
82     (hs : AEStronglyMeasurable s μ) (ht : AEStronglyMeasurable t μ) :
83     eLpNorm ((s+jump S a)-(t+jump T b)) p μ ≤ eLpNorm (s-t) p μ +
84       (‖a-b‖ₑ * μ S ^ (1/p.toReal) + ‖b‖ₑ * μ (S ∆ T) ^ (1/p.toReal)) := by
85   have he : (s+jump S a)-(t+jump T b) = (s-t)+(jump S a-jump T b) := by abel
86   rw [he]
87   exact (eLpNorm_add_le (hs.sub ht)
88     ((jump_measurable S hS a μ).sub (jump_measurable T hT b μ)) hp).trans
89       (add_le_add_right (finite_p_perturbation μ S T hS hT p hp hpTop a b) _)
90 
91 end KomorebiPaperV.MaskPerturbation

Back to source controls