On complemented subspaces of L1[0,1]L_1[0,1]

PL1/KernelTranslations.lean

All source files · Download exact source

SHA-256: acb95c46965ea416c6c99ef8cad6f226ea2e2b9e4c4548bc9bdd02edb563bdd1

1import PL1.FiniteCoordinateKernels2import PL1.ResolventAlmostInvariant34/-! # Finite translated probability densities and their exact average -/56noncomputable section7open MeasureTheory8open scoped ENNReal NNReal BigOperators910namespace PL1.FiniteCoordinateKernels11open Walsh Noise1213abbrev Assignments (S : Finset ℕ) := S → Sign1415def extend (S : Finset ℕ) (a : Assignments S) : Walsh.Group :=16  fun j => if h : j ∈ S then a ⟨j, h⟩ else 11718@[simp] theorem extend_apply (S : Finset ℕ) (a : Assignments S) (j : S) :19    extend S a j = a j := by simp [extend]2021theorem cylinder_extend_iff (S : Finset ℕ) (a : Assignments S) (x : Walsh.Group) :22    x ∈ cylinder S (extend S a) ↔ a = fun j : S => x j := by23  constructor24  · intro hx25    funext j26    exact ((extend_apply S a j).symm.trans (hx j j.property).symm)27  · rintro rfl j hj28    simp [extend, hj]2930theorem sum_kernel_extend (S : Finset ℕ) (x : Walsh.Group) :31    ∑ a : Assignments S, kernel S (extend S a) x = (2 : ℝ) ^ S.card := by32  classical33  rw [Finset.sum_eq_single (fun j : S => x j)]34  · rw [kernel_eq_indicator, Set.indicator_of_mem]35    exact (cylinder_extend_iff S _ x).mpr rfl36  · intro b _ hb37    rw [kernel_eq_indicator, Set.indicator_of_notMem]38    exact fun h => hb ((cylinder_extend_iff S b x).mp h)39  · simp4041theorem card_assignments (S : Finset ℕ) : Fintype.card (Assignments S) = 2 ^ S.card := by42  simp only [Assignments, Fintype.card_fun, Fintype.card_coe]43  congr 14445def translatedDensity (ν : Measure Walsh.Group) (S : Finset ℕ) (s : Walsh.Group) :46    C(Walsh.Group, ℝ) :=47  ⟨fun x => density ν S (s * x), (density ν S).continuous.comp (continuous_const.mul continuous_id)⟩4849theorem translatedDensity_apply (ν : Measure Walsh.Group) (S : Finset ℕ) (s x : Walsh.Group) :50    translatedDensity ν S s x = density ν S (s * x) := rfl5152theorem translatedDensity_eq_sum (ν : Measure Walsh.Group) (S : Finset ℕ) (s : Walsh.Group) :53    translatedDensity ν S s =54      ∑ F ∈ S.powerset, (coefficient ν F * character F s) • characterContinuous F := by55  ext x56  simp only [translatedDensity_apply, density_apply, character_mul,57    ContinuousMap.sum_apply, ContinuousMap.smul_apply, smul_eq_mul,58    characterContinuous, ContinuousMap.coe_mk, mul_assoc]5960theorem translatedDensity_nonneg (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]61    (S : Finset ℕ) (s x : Walsh.Group) : 0 ≤ translatedDensity ν S s x :=62  density_nonneg ν S (s * x)6364theorem integral_translatedDensity (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]65    (S : Finset ℕ) (s : Walsh.Group) : ∫ x, translatedDensity ν S s x ∂haar = 1 := by66  change (∫ x, density ν S (s * x) ∂haar) = 167  rw [integral_mul_left_eq_self, integral_density]6869theorem translatedDensity_eq_convolution (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]70    (S : Finset ℕ) (s : Walsh.Group) :71    ContinuousMap.toLp 1 haar ℝ (translatedDensity ν S s) =72      convolutionL1 ν (kernelL1 S s) := by73  rw [translatedDensity_eq_sum, kernelL1_eq_sum]74  simp only [map_sum, map_smul, toLp_characterContinuous, convolutionL1_character,75    smul_smul, mul_comm]7677theorem sum_translatedDensity (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]78    (S : Finset ℕ) (x : Walsh.Group) :79    ∑ a : Assignments S, translatedDensity ν S (extend S a) x = (2 : ℝ) ^ S.card := by80  have heq (s y : Walsh.Group) : kernel S y (s * x) = kernel S s (y * x) := by81    simp only [kernel_apply, character_mul]82    apply Finset.sum_congr rfl83    intro F hF84    ring85  have heq2 (a : Assignments S) : translatedDensity ν S (extend S a) x =86      ∫ y, kernel S (extend S a) (y * x) ∂ν := by87    rw [translatedDensity_apply, density_eq_integral]88    exact integral_congr_ae (ae_of_all _ (heq (extend S a)))89  rw [Finset.sum_congr rfl (fun a _ => heq2 a)]90  rw [← integral_finsetSum]91  · simp [sum_kernel_extend, integral_const, measureReal_def]92  · intro a _93    exact ((kernel S (extend S a)).continuous.comp (continuous_id.mul continuous_const)).integrable_of_hasCompactSupport94      (HasCompactSupport.of_compactSpace _)9596theorem average_translatedDensity (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]97    (S : Finset ℕ) (x : Walsh.Group) :98    (Fintype.card (Assignments S) : ℝ)⁻¹ *99      ∑ a : Assignments S, translatedDensity ν S (extend S a) x = 1 := by100  rw [sum_translatedDensity, card_assignments]101  push_cast102  exact inv_mul_cancel₀ (by positivity)103104theorem density_congr (ν : Measure Walsh.Group) (S : Finset ℕ) {x y : Walsh.Group}105    (hxy : ∀ j ∈ S, x j = y j) : density ν S x = density ν S y := by106  simp only [density_apply]107  apply Finset.sum_congr rfl108  intro F hF109  congr 1110  exact Finset.prod_congr rfl (fun j hj => congrArg signValue (hxy j111    ((Finset.mem_powerset.mp hF) hj)))112113theorem translatedDensity_congr (ν : Measure Walsh.Group) (S : Finset ℕ)114    (s : Walsh.Group) {x y : Walsh.Group} (hxy : ∀ j ∈ S, x j = y j) :115    translatedDensity ν S s x = translatedDensity ν S s y :=116  density_congr ν S (fun j hj => congrArg (fun z => s j * z) (hxy j hj))117118def translatedSet (B : Set Walsh.Group) (s : Walsh.Group) : Set Walsh.Group :=119  (fun x => s * x) ⁻¹' B120121theorem measurableSet_translatedSet {B : Set Walsh.Group} (hB : MeasurableSet B)122    (s : Walsh.Group) : MeasurableSet (translatedSet B s) :=123  hB.preimage (continuous_const.mul continuous_id).measurable124125theorem measure_translatedSet {B : Set Walsh.Group} (hB : MeasurableSet B)126    (s : Walsh.Group) : haar (translatedSet B s) = haar B :=127  (measurePreserving_mul_left haar s).measure_preimage hB.nullMeasurableSet128129theorem dependsOn_translatedSet (S : Finset ℕ) {B : Set Walsh.Group}130    (hB : DependsOn S B) (s : Walsh.Group) : DependsOn S (translatedSet B s) := by131  intro x y hxy132  exact hB (s * x) (s * y) (fun j hj => congrArg (fun z => s j * z) (hxy j hj))133134theorem setIntegral_translatedDensity (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]135    (S : Finset ℕ) {B : Set Walsh.Group} (hBm : MeasurableSet B) (hB : DependsOn S B)136    (s : Walsh.Group) :137    ∫ x in translatedSet B s, translatedDensity ν S s x ∂haar = ν.real B := by138  rw [← integral_indicator (measurableSet_translatedSet hBm s)]139  change (∫ x, B.indicator (density ν S) (s * x) ∂haar) = _140  rw [integral_mul_left_eq_self, integral_indicator hBm, setIntegral_density ν S hBm hB]141142theorem norm_noise_translatedResolventDensity_sub_le (rates : ℕ → ℝ≥0)143    (t : PositiveTime) (S : Finset ℕ) (s : Walsh.Group) (u : ℝ≥0) :144    let q := ContinuousMap.toLp 1 haar ℝ (translatedDensity (resolventMeasure rates t) S s)145    ‖noiseL1 ℝ rates u q - q‖ ≤ 2 * (1 - Real.exp (-(u : ℝ) / (t : ℝ))) := by146  let := isProbabilityMeasure_resolventMeasure rates t.property147  dsimp only148  rw [translatedDensity_eq_convolution]149  change ‖noiseL1 ℝ rates u (resolventL1 ℝ rates t (kernelL1 S s)) -150    resolventL1 ℝ rates t (kernelL1 S s)‖ ≤ _151  simpa only [norm_kernelL1, mul_one] using152    norm_noise_resolvent_sub_le ℝ rates t u (kernelL1 S s)153154end PL1.FiniteCoordinateKernels155