PL1/DyadicL1Coordinates.lean

All source files · Download exact source

SHA-256: 57be0e3229f6df5b21101ccefe3e17d75fbbff2daf0e443d7ed2bd31aa58b256

1import PL1.IntervalDyadicApproximation2import PL1.DyadicCellMeasure3import PL1.FiniteSummingFromMatrix45/-! Actual contractive finite ell1 coordinates for interval dyadic averages. -/67noncomputable section8open MeasureTheory9open scoped BigOperators ENNReal Topology1011namespace PL1.DyadicL1Coordinates12open PL1.DyadicTrace PL1.FiniteSumming13attribute [local instance] intervalMeasure_probability1415def normalizedVector (m : ℕ) (i : Fin (2 ^ m)) : IntervalL1 ℝ :=16  (2 : ℝ) ^ m • dyadicVector m i1718theorem norm_normalizedVector (m : ℕ) (i : Fin (2 ^ m)) :19    ‖normalizedVector m i‖ = 1 := by20  rw [normalizedVector, norm_smul, PartitionAverages.norm_vector]21  rw [measureReal_def, intervalMeasure_cell_toReal m i i.isLt]22  simp2324def synthesis (m : ℕ) : EllOne (2 ^ m) →L[ℝ] IntervalL1 ℝ :=25  ∑ i : Fin (2 ^ m), (PiLp.proj 1 (fun _ : Fin (2 ^ m) => ℝ) i).smulRight26    (normalizedVector m i)2728theorem synthesis_apply (m : ℕ) (x : EllOne (2 ^ m)) :29    synthesis m x = ∑ i, x i • normalizedVector m i := by30  simp [synthesis]3132theorem norm_synthesis_le_one (m : ℕ) : ‖synthesis m‖ ≤ 1 := by33  apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one34  intro x35  rw [one_mul, synthesis_apply, norm_ellOne]36  calc37    _ ≤ ∑ i, ‖x i • normalizedVector m i‖ := norm_sum_le _ _38    _ = _ := by simp [norm_smul, norm_normalizedVector, Real.norm_eq_abs]3940def analysisLinear (m : ℕ) : IntervalL1 ℝ →ₗ[ℝ] EllOne (2 ^ m) :=41  (WithLp.linearEquiv 1 ℝ (Fin (2 ^ m) → ℝ)).symm.toLinearMap.comp42    (LinearMap.pi (fun i : Fin (2 ^ m) =>43      (TraceBounds.cellFunctional (𝕜 := ℝ) intervalMeasure (cell m)44        (measurableSet_cell m) i).toLinearMap))4546theorem analysisLinear_apply (m : ℕ) (f : IntervalL1 ℝ) (i : Fin (2 ^ m)) :47    analysisLinear m f i = TraceBounds.cellFunctional intervalMeasure (cell m)48      (measurableSet_cell m) i f := rfl4950theorem norm_analysisLinear_le (m : ℕ) (f : IntervalL1 ℝ) :51    ‖analysisLinear m f‖ ≤ ‖f‖ := by52  rw [norm_ellOne]53  simp_rw [analysisLinear_apply, ← Real.norm_eq_abs]54  rw [← Finset.sum_range (fun i => ‖TraceBounds.cellFunctional (𝕜 := ℝ)55    intervalMeasure (cell m) (measurableSet_cell m) i f‖)]56  calc57    _ ≤ ∑ i ∈ Finset.range (2 ^ m),58        ‖L1Masks.mask intervalMeasure (cell m i) (measurableSet_cell m i) f‖ := by59      apply Finset.sum_le_sum60      intro i hi61      exact TraceBounds.norm_cellFunctional_apply_le_mask intervalMeasure (cell m)62        (measurableSet_cell m) i f63    _ ≤ ‖f‖ := L1Masks.sum_norm_mask_le intervalMeasure (Finset.range (2 ^ m))64      (cell m) (measurableSet_cell m) (pairwiseDisjoint_cell m) f6566def analysis (m : ℕ) : IntervalL1 ℝ →L[ℝ] EllOne (2 ^ m) :=67  (analysisLinear m).mkContinuous 1 (by68    intro f69    simpa using norm_analysisLinear_le m f)7071theorem analysis_apply (m : ℕ) (f : IntervalL1 ℝ) (i : Fin (2 ^ m)) :72    analysis m f i = TraceBounds.cellFunctional intervalMeasure (cell m)73      (measurableSet_cell m) i f := rfl7475theorem norm_analysis_le_one (m : ℕ) : ‖analysis m‖ ≤ 1 := by76  apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one77  intro f78  simpa [analysis] using norm_analysisLinear_le m f7980theorem synthesis_analysis (m : ℕ) (f : IntervalL1 ℝ) :81    synthesis m (analysis m f) = dyadicAverage m f := by82  rw [synthesis_apply]83  simp_rw [analysis_apply, normalizedVector, smul_smul]84  rw [← Finset.sum_range (fun i => (TraceBounds.cellFunctional (𝕜 := ℝ)85    intervalMeasure (cell m) (measurableSet_cell m) i f * (2 : ℝ) ^ m) • dyadicVector m i)]86  rw [dyadicAverage, PartitionAverages.average_apply]87  apply Finset.sum_congr rfl88  intro i hi89  have hi' : i < 2 ^ m := Finset.mem_range.mp hi90  rw [PartitionAverages.coefficient, smul_apply]91  rw [measureReal_def, intervalMeasure_cell_toReal m i hi']92  simp [mul_comm, smul_eq_mul]9394theorem cellFunctional_normalizedVector (m : ℕ) (i j : Fin (2 ^ m)) :95    TraceBounds.cellFunctional (𝕜 := ℝ) intervalMeasure (cell m) (measurableSet_cell m)96      i (normalizedVector m j) = if i = j then 1 else 0 := by97  rw [normalizedVector, map_smul,98    PartitionAverages.cellFunctional_vector intervalMeasure (cell m)99      (measurableSet_cell m) (pairwiseDisjoint_cell m)]100  by_cases hij : i = j101  · subst j102    simp only [ite_true, smul_eq_mul, measureReal_def]103    rw [intervalMeasure_cell_toReal m i i.isLt]104    exact mul_inv_cancel₀ (pow_ne_zero _ (by norm_num))105  · have hval : (i : ℕ) ≠ j := fun h => hij (Fin.ext h)106    simp [hij, hval]107108theorem analysis_synthesis (m : ℕ) (x : EllOne (2 ^ m)) :109    analysis m (synthesis m x) = x := by110  ext i111  rw [analysis_apply, synthesis_apply, map_sum]112  simp only [map_smul, cellFunctional_normalizedVector, smul_eq_mul,113    mul_ite, mul_one, mul_zero]114  simp115116theorem norm_synthesis (m : ℕ) (x : EllOne (2 ^ m)) :117    ‖synthesis m x‖ = ‖x‖ := by118  apply le_antisymm119  · exact ((synthesis m).le_opNorm x).trans (by120      simpa using mul_le_mul_of_nonneg_right (norm_synthesis_le_one m) (norm_nonneg x))121  · calc122      ‖x‖ = ‖analysis m (synthesis m x)‖ := congrArg norm (analysis_synthesis m x).symm123      _ ≤ ‖synthesis m x‖ := by124        exact ((analysis m).le_opNorm _).trans (by125          simpa using mul_le_mul_of_nonneg_right (norm_analysis_le_one m) (norm_nonneg _))126127end PL1.DyadicL1Coordinates128