PL1/EnfloNoL1.lean

All source files · Download exact source

SHA-256: fbc5daf1717912a985ce1bfe025bd96febea6a65f457976100128d08729ef42d

1import PL1.EnfloCopyExclusion2import PL1.EnfloSmoothing3import PL1.PartialMainTheorems4import PL1.ComplementedLatticeReduction56/-! # Actual exclusion of arbitrary interval L1 copies in the constant-rate example78Positive-time noise decay is proved for every real L1 source operator. The9resolvent and intrinsic-coordinate arguments then exclude bounded-below maps,10and actual range equivalences transport the conclusion to interval L1.11-/12noncomputable section13set_option backward.isDefEq.respectTransparency false14open MeasureTheory15open scoped NNReal ENNReal16namespace PL1.Noise17open Walsh EnfloBush1819/-- Every actual dyadic constant-rate resolvent has the full arbitrary-source20maximum-mass decay required by the intrinsic argument. -/21theorem constant_dyadicOperator_comp_dyadicVanishing22    (n : ℕ) (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) :23    DyadicVanishing (((dyadicSystem ℝ constantRates).operator n).comp S) :=24  dyadicVanishing_resolvent_of_noise constantRates noise_comp_dyadicVanishing (dyadicTime n) S2526theorem constant_intrinsic_no_real_L1 (K : Type*) [RCLike K] :27    ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) (dyadicSystem K constantRates).IntrinsicSpace :=28  scalarIntrinsic_no_real_L1_of_operators K constantRates constant_dyadicOperator_comp_dyadicVanishing2930theorem constant_projection_range_no_real_L1 (K : Type*) [RCLike K] :31    ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) (projection K constantRates).range := by32  change ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) (dyadicSystem K constantRates).projection.range33  rw [DyadicSystem.projection_range]34  exact constant_intrinsic_no_real_L1 K3536/-- Restriction of the actual range equivalence to the compatible real actions.37The pinned continuous-equivalence restriction API only handles endomorphisms,38so the two different range types are bundled explicitly. -/39def intervalProjectionRangeRealEquiv (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0) :40    (projection K rates).range ≃L[ℝ] (intervalProjection K rates).range where41  toLinearEquiv := (intervalProjectionRangeEquiv K rates).toLinearEquiv.restrictScalars ℝ42  continuous_toFun := (intervalProjectionRangeEquiv K rates).continuous43  continuous_invFun := (intervalProjectionRangeEquiv K rates).symm.continuous44/-- Even the natural real Banach space underlying the real or complex45interval projection range contains no closed isomorphic real interval-L1 copy. -/46theorem constant_intervalProjection_range_no_real_L1 (K : Type*) [RCLike K] :47    ¬ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) (intervalProjection K constantRates).range := by48  intro hc49  exact constant_projection_range_no_real_L1 K50    (hc.map (intervalProjectionRangeRealEquiv K constantRates).symm)5152/-- The same no-copy result with the explicitly restricted scalar convention53used in the reviewed theorem statements. -/54theorem constant_intervalProjection_range_no_underlying_real_L1 (K : Type*) [RCLike K] :55    ¬ @ContainsIsomorphicCopy ℝ _ (IntervalL1 ℝ) _ _56      (UnderlyingReal K (intervalProjection K constantRates).range)57      (inferInstanceAs (NormedAddCommGroup (intervalProjection K constantRates).range))58      (NormedSpace.restrictScalars ℝ K (intervalProjection K constantRates).range) := by59  intro hc60  exact constant_intervalProjection_range_no_real_L1 K61    (hc.map (ComplementedLattice.naturalToUnderlyingReal (K := K)62      (intervalProjection K constantRates).range).symm)6364/-- In particular no scalar interval-L1 copy exists, with the original scalar65field and the original interval projection range norm. -/66theorem constant_intervalProjection_range_no_L1 (K : Type*) [RCLike K] :67    ¬ ContainsIsomorphicCopy K (IntervalL1 K) (intervalProjection K constantRates).range := by68  let : CompleteSpace (intervalProjection K constantRates).range :=69    (intervalProjection_range_isClosed K constantRates).isComplete.completeSpace_coe70  intro hc71  exact constant_intervalProjection_range_no_real_L1 K72    (ComplementedLattice.scalar_L1_copy_contains_real_L1 hc)7374#print axioms constant_intervalProjection_range_no_real_L175#print axioms constant_intervalProjection_range_no_underlying_real_L176#print axioms constant_intervalProjection_range_no_L177end PL1.Noise7879