PL1/EnfloCopyExclusion.lean

All source files · Download exact source

SHA-256: 8593a68daadfd8490392163ab781b8c9627ca54bff130ae99250863ba592d51d

1import PL1.EnfloIntrinsic2import PL1.EnfloTwoMaps3import PL1.IntrinsicRealParts45/-! From dyadic decay to exclusion of arbitrary closed real L1 copies. -/67noncomputable section8set_option backward.isDefEq.respectTransparency false9open MeasureTheory Filter10open scoped BigOperators Topology ENNReal NNReal1112namespace PL1.EnfloBush1314theorem exists_boundedBelow_of_containsIsomorphicCopy15    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]16    [NormedAddCommGroup F] [NormedSpace ℝ F]17    (h : ContainsIsomorphicCopy ℝ E F) :18    ∃ (T : E →L[ℝ] F) (c : ℝ), 0 < c ∧ ∀ x, c * ‖x‖ ≤ ‖T x‖ := by19  obtain ⟨V, _, ⟨e⟩⟩ := h20  let N := ‖e.symm.toContinuousLinearMap‖21  have hN : 0 < N + 1 := by dsimp [N]; positivity22  refine ⟨V.subtypeL.comp e.toContinuousLinearMap, (N + 1)⁻¹, inv_pos.mpr hN, ?_⟩23  intro x24  change (N + 1)⁻¹ * ‖x‖ ≤ ‖e x‖25  rw [inv_mul_eq_div, div_le_iff₀ hN]26  have he : ‖x‖ ≤ N * ‖e x‖ := by27    simpa only [ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.symm_apply_apply] using28      e.symm.toContinuousLinearMap.le_opNorm (e x)29  nlinarith [norm_nonneg (e x)]3031theorem not_containsIsomorphicCopy_of_no_boundedBelow32    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]33    (h : ∀ (T : IntervalL1 ℝ →L[ℝ] E) (c : ℝ), 0 < c →34      (∀ f, c * ‖f‖ ≤ ‖T f‖) → False) :35    ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by36  intro hc37  obtain ⟨T, c, hc, hlower⟩ := exists_boundedBelow_of_containsIsomorphicCopy hc38  exact h T c hc hlower3940open Walsh Noise IntrinsicRealParts4142theorem not_boundedBelow_scalarIntrinsic_of_operators (K : Type*) [RCLike K]43    (rates : ℕ → ℝ≥0)44    (hS : ∀ n (A : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar),45      DyadicVanishing (((dyadicSystem ℝ rates).operator n).comp A))46    (T : IntervalL1 ℝ →L[ℝ] (dyadicSystem K rates).IntrinsicSpace)47    {c : ℝ} (hc : 0 < c) (hlower : ∀ f, c * ‖f‖ ≤ ‖T f‖) : False := by48  let : SFinite (IntervalModel.disjointMeasure haar) := by49    dsimp only [IntervalModel.disjointMeasure]50    infer_instance51  let F := (IntervalModel.flattenIsometry (𝕜 := ℝ) haar).toContinuousLinearMap52  let J := (dyadicSystem ℝ rates).inclusion.toContinuousLinearMap53  let A := (realPart K rates).comp T54  let B := (imagPart K rates).comp T55  apply not_boundedBelow_two_maps (IntervalModel.disjointMeasure haar)56    (F.comp (J.comp A)) (F.comp (J.comp B))57    (dyadicVanishing_intrinsic_flatten haar (dyadicSystem ℝ rates) hS A)58    (dyadicVanishing_intrinsic_flatten haar (dyadicSystem ℝ rates) hS B) hc59  intro f60  have hf := (hlower f).trans (norm_le_parts K rates (T f))61  simpa only [F, J, A, B, ContinuousLinearMap.comp_apply,62    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map] using hf6364theorem scalarIntrinsic_no_real_L1_of_operators (K : Type*) [RCLike K]65    (rates : ℕ → ℝ≥0)66    (hS : ∀ n (A : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar),67      DyadicVanishing (((dyadicSystem ℝ rates).operator n).comp A)) :68    ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) (dyadicSystem K rates).IntrinsicSpace :=69  not_containsIsomorphicCopy_of_no_boundedBelow (fun T _ hc hlower =>70    not_boundedBelow_scalarIntrinsic_of_operators K rates hS T hc hlower)7172#print axioms scalarIntrinsic_no_real_L1_of_operators73end PL1.EnfloBush747576