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

PL1/FiniteCoordinateKernels.lean

All source files · Download exact source

SHA-256: 241fcdccd4a25dbf8caa8270800a5e9aa6a66c59d3afbb4a67df8a788c1f90e2

1import PL1.ExplicitMartingale23/-!4# Finite-coordinate probability kernels56Arbitrary finite coordinate sets are allowed, so all constructions apply7beyond a prescribed initial segment. Convolution with an arbitrary probability8measure gives a nonnegative finite Walsh polynomial of Haar integral one.9-/1011noncomputable section12open MeasureTheory13open scoped ENNReal BigOperators1415namespace PL1.FiniteCoordinateKernels16open Walsh1718def cylinder (S : Finset ℕ) (s : Walsh.Group) : Set Walsh.Group :=19  {x | ∀ j ∈ S, x j = s j}2021def kernel (S : Finset ℕ) (s : Walsh.Group) : C(Walsh.Group, ℝ) :=22  ∑ F ∈ S.powerset, character F s • characterContinuous F2324theorem kernel_apply (S : Finset ℕ) (s x : Walsh.Group) :25    kernel S s x = ∑ F ∈ S.powerset, character F s * character F x := by26  simp only [kernel, ContinuousMap.sum_apply, ContinuousMap.smul_apply,27    smul_eq_mul, characterContinuous, ContinuousMap.coe_mk]2829theorem kernel_eq_indicator (S : Finset ℕ) (s x : Walsh.Group) :30    kernel S s x = (cylinder S s).indicator (fun _ => (2 : ℝ) ^ S.card) x := by31  classical32  have heq : kernel S s x = ∏ j ∈ S, (1 + signValue (s j * x j)) := by33    rw [kernel_apply, Finset.prod_one_add]34    apply Finset.sum_congr rfl35    intro F hF36    exact (character_mul F s x).symm37  rw [heq]38  simp_rw [ExplicitMartingale.one_add_sign_mul]39  by_cases hx : x ∈ cylinder S s40  · rw [Set.indicator_of_mem hx]41    simp only [Finset.prod_congr rfl (fun j hj => ite_eq_left (hx j hj)), Finset.prod_const]42  · rw [Set.indicator_of_notMem hx]43    have h : ∃ j ∈ S, x j ≠ s j := by44      simpa only [cylinder, Set.mem_ofPred_eq, not_forall, exists_prop] using hx45    obtain ⟨j, hj, hneq⟩ := h46    exact Finset.prod_eq_zero hj (ite_eq_right hneq)4748theorem kernel_nonneg (S : Finset ℕ) (s x : Walsh.Group) : 0 ≤ kernel S s x := by49  rw [kernel_eq_indicator]50  exact Set.indicator_nonneg (fun _ _ => by positivity) _5152theorem integral_kernel (S : Finset ℕ) (s : Walsh.Group) :53    ∫ x, kernel S s x ∂haar = 1 := by54  simp_rw [kernel_apply]55  rw [integral_finsetSum _ (fun F _ => (integrable_character F).const_mul _)]56  simp_rw [integral_const_mul, Walsh.integral_character]57  simp5859def kernelL1 (S : Finset ℕ) (s : Walsh.Group) : Lp ℝ 1 haar :=60  ContinuousMap.toLp 1 haar ℝ (kernel S s)6162theorem coeFn_kernelL1 (S : Finset ℕ) (s : Walsh.Group) :63    kernelL1 S s =ᵐ[haar] kernel S s := ContinuousMap.coeFn_toLp haar _6465theorem kernelL1_eq_sum (S : Finset ℕ) (s : Walsh.Group) :66    kernelL1 S s = ∑ F ∈ S.powerset, character F s • characterLp 1 F := by67  simp only [kernelL1, kernel, map_sum, map_smul, toLp_characterContinuous]6869theorem norm_kernelL1 (S : Finset ℕ) (s : Walsh.Group) : ‖kernelL1 S s‖ = 1 := by70  rw [L1.norm_eq_integral_norm]71  calc72    _ = ∫ x, kernel S s x ∂haar := by73      apply integral_congr_ae74      filter_upwards [coeFn_kernelL1 S s] with x hx75      rw [hx, Real.norm_of_nonneg (kernel_nonneg S s x)]76    _ = 1 := integral_kernel S s7778def density (ν : Measure Walsh.Group) (S : Finset ℕ) : C(Walsh.Group, ℝ) :=79  ∑ F ∈ S.powerset, coefficient ν F • characterContinuous F8081theorem density_apply (ν : Measure Walsh.Group) (S : Finset ℕ) (x : Walsh.Group) :82    density ν S x = ∑ F ∈ S.powerset, coefficient ν F * character F x := by83  simp only [density, ContinuousMap.sum_apply, ContinuousMap.smul_apply,84    smul_eq_mul, characterContinuous, ContinuousMap.coe_mk]8586theorem density_eq_integral (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]87    (S : Finset ℕ) (x : Walsh.Group) :88    density ν S x = ∫ y, kernel S y x ∂ν := by89  simp_rw [density_apply, kernel_apply]90  have hchar (F : Finset ℕ) : Integrable (character F) ν :=91    (characterContinuous F).continuous.integrable_of_hasCompactSupport92      (HasCompactSupport.of_compactSpace _)93  rw [integral_finsetSum _ (fun F _ => (hchar F).mul_const _)]94  simp only [integral_mul_const, coefficient]9596theorem density_nonneg (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]97    (S : Finset ℕ) (x : Walsh.Group) : 0 ≤ density ν S x := by98  rw [density_eq_integral]99  exact integral_nonneg (fun y => kernel_nonneg S y x)100101theorem integral_density (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]102    (S : Finset ℕ) : ∫ x, density ν S x ∂haar = 1 := by103  simp_rw [density_apply]104  rw [integral_finsetSum _ (fun F _ => (integrable_character F).const_mul _)]105  simp_rw [integral_const_mul, Walsh.integral_character]106  simp [coefficient]107108theorem density_eq_convolution (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]109    (S : Finset ℕ) :110    ContinuousMap.toLp 1 haar ℝ (density ν S) = convolutionL1 ν (kernelL1 S 1) := by111  simp only [density, map_sum, map_smul, toLp_characterContinuous,112    kernelL1_eq_sum, character_one, one_smul, convolutionL1_character]113114/-- A set genuinely depends only on the displayed finite coordinates. -/115def DependsOn (S : Finset ℕ) (B : Set Walsh.Group) : Prop :=116  ∀ x y : Walsh.Group, (∀ j ∈ S, x j = y j) → (x ∈ B ↔ y ∈ B)117118theorem indicator_kernel (S : Finset ℕ) {B : Set Walsh.Group} (hB : DependsOn S B)119    (y x : Walsh.Group) :120    B.indicator (kernel S y) x = B.indicator (fun _ => kernel S y x) y := by121  classical122  by_cases hxy : x ∈ cylinder S y123  · have hiff := hB x y hxy124    by_cases hy : y ∈ B125    · rw [Set.indicator_of_mem hy, Set.indicator_of_mem (hiff.mpr hy)]126    · rw [Set.indicator_of_notMem hy, Set.indicator_of_notMem (fun hx => hy (hiff.mp hx))]127  · have hk : kernel S y x = 0 := by128      rw [kernel_eq_indicator, Set.indicator_of_notMem hxy]129    simp only [Set.indicator_apply, hk, ite_self]130131theorem setIntegral_kernel (S : Finset ℕ) {B : Set Walsh.Group}132    (hBm : MeasurableSet B) (hB : DependsOn S B) (y : Walsh.Group) :133    ∫ x in B, kernel S y x ∂haar = B.indicator (fun _ => (1 : ℝ)) y := by134  classical135  rw [← integral_indicator hBm]136  simp_rw [indicator_kernel S hB y]137  by_cases hy : y ∈ B138  · simp only [Set.indicator_of_mem hy, integral_kernel]139  · simp only [integral_zero, Set.indicator_of_notMem hy]140141theorem setIntegral_density (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]142    (S : Finset ℕ) {B : Set Walsh.Group} (hBm : MeasurableSet B) (hB : DependsOn S B) :143    ∫ x in B, density ν S x ∂haar = ν.real B := by144  have hc : Continuous (fun z : Walsh.Group × Walsh.Group => kernel S z.2 z.1) := by145    simp only [kernel_apply]146    exact continuous_finsetSum _ (fun F _ =>147      ((characterContinuous F).continuous.comp continuous_snd).mul148        ((characterContinuous F).continuous.comp continuous_fst))149  have hi : Integrable (fun z : Walsh.Group × Walsh.Group => kernel S z.2 z.1)150      ((haar.restrict B).prod ν) :=151    hc.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)152  simp_rw [density_eq_integral]153  rw [integral_integral_swap hi]154  simp_rw [setIntegral_kernel S hBm hB]155  rw [integral_indicator hBm, integral_const]156  simp157158end PL1.FiniteCoordinateKernels159