PL1/EnfloStarbirdDyadic.lean

All source files · Download exact source

SHA-256: 8c8688b562e83033a0627ee3b27b6149f35a3b55f2b4488596013fe3114e1a28

1import PL1.EnfloStarbirdProjection2import PL1.IntervalDyadicApproximation34/-! # Dyadic verification of the quantitative Enflo–Starbird projection criterion56The operator norm on genuine interval L1 is controlled by its values on dyadic7indicators. Consequently a uniformly small dyadic reconstruction error gives8an actual complemented copy, with an explicit Neumann-series projection.9The disjoint-tree extraction from an arbitrary embedding remains separate.10-/1112noncomputable section13open MeasureTheory Filter14open scoped BigOperators Topology1516namespace PL1.EnfloStarbird17open DyadicTrace1819variable {𝕜 : Type*} [RCLike 𝕜]20variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]2122attribute [local instance] intervalMeasure_probability2324private theorem sum_norm_dyadic_pieces_le (n : ℕ) (f : IntervalL1 𝕜) :25    (∑ i ∈ Finset.range (2 ^ n),26      ‖PartitionAverages.coefficient intervalMeasure (cell n) (measurableSet_cell n) i f •27        dyadicVector (𝕜 := 𝕜) n i‖) ≤ ‖f‖ := by28  calc29    _ ≤ ∑ i ∈ Finset.range (2 ^ n),30        ‖TraceBounds.cellFunctional intervalMeasure (cell n) (measurableSet_cell n) i f‖ :=31      Finset.sum_le_sum (fun i _ => PartitionAverages.norm_coefficient_smul_vector_le32        intervalMeasure (cell n) (measurableSet_cell n) i f)33    _ ≤ ∑ i ∈ Finset.range (2 ^ n),34        ‖L1Masks.mask intervalMeasure (cell n i) (measurableSet_cell n i) f‖ :=35      Finset.sum_le_sum (fun i _ => TraceBounds.norm_cellFunctional_apply_le_mask36        intervalMeasure (cell n) (measurableSet_cell n) i f)37    _ ≤ ‖f‖ := L1Masks.sum_norm_mask_le intervalMeasure _ _ _ (pairwiseDisjoint_cell n) f3839/-- It suffices to check the L1 operator bound on all genuine dyadic indicators. -/40theorem opNorm_le_of_dyadic_vectors (T : IntervalL1 𝕜 →L[𝕜] E) (C : ℝ) (hC : 0 ≤ C)41    (hT : ∀ n i, i < 2 ^ n → ‖T (dyadicVector (𝕜 := 𝕜) n i)‖ ≤42      C * ‖dyadicVector (𝕜 := 𝕜) n i‖) : ‖T‖ ≤ C := by43  have ha (n : ℕ) (f : IntervalL1 𝕜) : ‖T (dyadicAverage n f)‖ ≤ C * ‖f‖ := by44    rw [PartitionAverages.average_apply, map_sum]45    calc46      _ ≤ ∑ i ∈ Finset.range (2 ^ n),47          ‖T (PartitionAverages.coefficient intervalMeasure (cell n) (measurableSet_cell n) i f •48            dyadicVector (𝕜 := 𝕜) n i)‖ := norm_sum_le _ _49      _ ≤ ∑ i ∈ Finset.range (2 ^ n), C *50          ‖PartitionAverages.coefficient intervalMeasure (cell n) (measurableSet_cell n) i f •51            dyadicVector (𝕜 := 𝕜) n i‖ := by52        apply Finset.sum_le_sum53        intro i hi54        rw [map_smul, norm_smul, norm_smul]55        calc56          _ ≤ ‖PartitionAverages.coefficient (𝕜 := 𝕜) intervalMeasure (cell n)57                (measurableSet_cell n) i f‖ * (C * ‖dyadicVector (𝕜 := 𝕜) n i‖) :=58            mul_le_mul_of_nonneg_left (hT n i (Finset.mem_range.mp hi)) (norm_nonneg _)59          _ = _ := by ring60      _ = C * ∑ i ∈ Finset.range (2 ^ n),61          ‖PartitionAverages.coefficient intervalMeasure (cell n) (measurableSet_cell n) i f •62            dyadicVector (𝕜 := 𝕜) n i‖ := (Finset.mul_sum _ _ _).symm63      _ ≤ C * ‖f‖ := mul_le_mul_of_nonneg_left (sum_norm_dyadic_pieces_le n f) hC64  apply ContinuousLinearMap.opNorm_le_bound T hC65  intro f66  exact le_of_tendsto ((T.continuous.tendsto f).comp (dyadicAverage_tendsto f)).norm67    (Filter.Eventually.of_forall (fun n => ha n f))6869theorem opNorm_le_iff_dyadic_vectors (T : IntervalL1 𝕜 →L[𝕜] E) (C : ℝ) (hC : 0 ≤ C) :70    ‖T‖ ≤ C ↔ ∀ n i, i < 2 ^ n → ‖T (dyadicVector (𝕜 := 𝕜) n i)‖ ≤71      C * ‖dyadicVector (𝕜 := 𝕜) n i‖ := by72  constructor73  · intro h n i _74    exact (T.le_opNorm _).trans (mul_le_mul_of_nonneg_right h (norm_nonneg _))75  · exact opNorm_le_of_dyadic_vectors T C hC7677/-- Dyadic reconstruction errors below one give a complemented copy of actual interval L1. -/78def complementedCopyOfDyadicError (J : IntervalL1 𝕜 →L[𝕜] E)79    (R : E →L[𝕜] IntervalL1 𝕜) (ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε < 1)80    (herror : ∀ n i, i < 2 ^ n →81      ‖dyadicVector (𝕜 := 𝕜) n i - R (J (dyadicVector (𝕜 := 𝕜) n i))‖ ≤82        ε * ‖dyadicVector (𝕜 := 𝕜) n i‖) : ComplementedCopy 𝕜 (IntervalL1 𝕜) E :=83  complementedCopyOfApproximateInverse J R84    ((opNorm_le_of_dyadic_vectors (1 - R.comp J) ε hε herror).trans_lt hε1)8586theorem closedComplemented_range_of_dyadicError (J : IntervalL1 𝕜 →L[𝕜] E)87    (R : E →L[𝕜] IntervalL1 𝕜) (ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε < 1)88    (herror : ∀ n i, i < 2 ^ n →89      ‖dyadicVector (𝕜 := 𝕜) n i - R (J (dyadicVector (𝕜 := 𝕜) n i))‖ ≤90        ε * ‖dyadicVector (𝕜 := 𝕜) n i‖) : J.range.ClosedComplemented :=91  (complementedCopyOfDyadicError J R ε hε hε1 herror).closedComplemented_range9293#print axioms opNorm_le_iff_dyadic_vectors94#print axioms complementedCopyOfDyadicError9596end PL1.EnfloStarbird97