PL1/L1Masks.lean
All source files · Download exact source
SHA-256: f296b8352fa882751d31dfbd247d54f72184015d7dba169c47e90796477c227f
1import PL1.Definitions2import Mathlib.MeasureTheory.Integral.Bochner.Set34/-! # Contractive measurable-set masks on actual scalar L1 spaces -/56noncomputable section7open MeasureTheory8open scoped ENNReal BigOperators910namespace PL1.L1Masks1112variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]13variable (μ : Measure Ω) (A : Set Ω) (hA : MeasurableSet A)1415def maskFun (f : Lp 𝕜 1 μ) : Lp 𝕜 1 μ :=16 ((L1.integrable_coeFn f).indicator hA).toL1 (A.indicator f)1718theorem coeFn_maskFun (f : Lp 𝕜 1 μ) : maskFun μ A hA f =ᵐ[μ] A.indicator f :=19 ((L1.integrable_coeFn f).indicator hA).coeFn_toL12021theorem maskFun_add (f g : Lp 𝕜 1 μ) :22 maskFun μ A hA (f + g) = maskFun μ A hA f + maskFun μ A hA g := by23 apply Lp.ext24 filter_upwards [coeFn_maskFun μ A hA (f + g), coeFn_maskFun μ A hA f,25 coeFn_maskFun μ A hA g, Lp.coeFn_add f g,26 Lp.coeFn_add (maskFun μ A hA f) (maskFun μ A hA g)] with x hfg hf hg ha hb27 have ha' : (f + g) x = f x + g x := ha28 have hb' : (maskFun μ A hA f + maskFun μ A hA g) x =29 maskFun μ A hA f x + maskFun μ A hA g x := hb30 rw [hfg, hb', hf, hg]31 by_cases hx : x ∈ A32 · simp only [Set.indicator_of_mem hx]33 exact ha'34 · simp only [Set.indicator_of_notMem hx, zero_add]3536theorem maskFun_smul (c : 𝕜) (f : Lp 𝕜 1 μ) :37 maskFun μ A hA (c • f) = c • maskFun μ A hA f := by38 apply Lp.ext39 filter_upwards [coeFn_maskFun μ A hA (c • f), coeFn_maskFun μ A hA f,40 Lp.coeFn_smul c f, Lp.coeFn_smul c (maskFun μ A hA f)] with x hcf hf ha hb41 have ha' : (c • f) x = c • f x := ha42 have hb' : (c • maskFun μ A hA f) x = c • maskFun μ A hA f x := hb43 rw [hcf, hb', hf]44 by_cases hx : x ∈ A45 · simp only [Set.indicator_of_mem hx]46 exact ha'47 · simp only [Set.indicator_of_notMem hx, smul_zero]4849theorem norm_maskFun (f : Lp 𝕜 1 μ) : ‖maskFun μ A hA f‖ = ∫ x in A, ‖f x‖ ∂μ := by50 rw [maskFun, L1.norm_of_fun_eq_integral_norm]51 simp_rw [norm_indicator_eq_indicator_norm]52 exact integral_indicator hA5354theorem norm_maskFun_le (f : Lp 𝕜 1 μ) : ‖maskFun μ A hA f‖ ≤ ‖f‖ := by55 rw [norm_maskFun, L1.norm_eq_integral_norm]56 exact setIntegral_le_integral (L1.integrable_coeFn f).norm57 (ae_of_all _ (fun x => norm_nonneg _))5859/-- Multiplication by a measurable-set indicator, on L1 equivalence classes. -/60def mask : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ :=61 LinearMap.mkContinuous62 { toFun := maskFun μ A hA63 map_add' := maskFun_add μ A hA64 map_smul' := maskFun_smul μ A hA }65 1 (fun f => by66 change ‖maskFun μ A hA f‖ ≤ 1 * ‖f‖67 simpa only [one_mul] using norm_maskFun_le μ A hA f)6869theorem coeFn_mask (f : Lp 𝕜 1 μ) : mask μ A hA f =ᵐ[μ] A.indicator f :=70 coeFn_maskFun μ A hA f7172theorem norm_mask (f : Lp 𝕜 1 μ) : ‖mask μ A hA f‖ = ∫ x in A, ‖f x‖ ∂μ :=73 norm_maskFun μ A hA f7475theorem norm_mask_le_one : ‖mask (𝕜 := 𝕜) μ A hA‖ ≤ 1 :=76 ContinuousLinearMap.opNorm_le_bound _ zero_le_one77 (fun f => by78 change ‖maskFun μ A hA f‖ ≤ 1 * ‖f‖79 simpa only [one_mul] using norm_maskFun_le μ A hA f)8081/-- Disjoint masks divide, rather than duplicate, the L1 norm. -/82theorem sum_norm_mask_le {ι : Type*} (s : Finset ι) (sets : ι → Set Ω)83 (hsets : ∀ i, MeasurableSet (sets i))84 (hdisj : Pairwise (fun i j => Disjoint (sets i) (sets j))) (f : Lp 𝕜 1 μ) :85 (∑ i ∈ s, ‖mask μ (sets i) (hsets i) f‖) ≤ ‖f‖ := by86 simp only [norm_mask]87 rw [← integral_biUnion_finset s (fun i _ => hsets i)88 (fun i _ j _ hij => hdisj hij) (fun i _ => (L1.integrable_coeFn f).norm.integrableOn)]89 rw [L1.norm_eq_integral_norm]90 exact setIntegral_le_integral (L1.integrable_coeFn f).norm91 (ae_of_all _ (fun x => norm_nonneg _))9293end PL1.L1Masks94