PL1/ComplementedLatticeRealTrace.lean
All source files · Download exact source
SHA-256: 0d4215abd8f486bbb6f29b2fcce395cdf9c5aec23c1c88114ee010ca99329ee4
1import PL1.ConstantNoiseTrace2import PL1.EnfloStarbirdProjection3import Mathlib.Analysis.RCLike.Extend45/-! # The real trace obstruction underlying the scalar construction67A scalar vanishing-trace operator also has vanishing trace after restricting scalars.8The proof extends the two real factor maps and takes real parts of the dyadic traces.9This is an operator statement and requires no classification of complex L1 spaces.10-/1112noncomputable section13open MeasureTheory Filter14open scoped ENNReal Topology1516namespace PL1.ComplementedLattice1718attribute [local instance] DyadicTrace.intervalMeasure_probability1920variable {K : Type*} [RCLike K]21variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace K E]22 [NormedSpace ℝ E] [IsScalarTower ℝ K E]23 [NormedAddCommGroup F] [NormedSpace K F]24 [NormedSpace ℝ F] [IsScalarTower ℝ K F]2526/-- Scalar-linear part of a real-linear operator. Its normalization is chosen to27recover real-valued inputs without a factor of two. -/28def scalarLinearPart (A : E →L[ℝ] F) : E →L[K] F :=29 let f : E → F := fun x => A x - (RCLike.I : K) • A ((RCLike.I : K) • x)30 have hadd (x y) : f (x + y) = f x + f y := by31 simp only [f, smul_add, map_add]32 abel33 have hreal (c : ℝ) (x : E) : f ((c : K) • x) = (c : K) • f x := by34 simp only [f, ← RCLike.real_smul_eq_coe_smul, map_smul, smul_sub,35 smul_comm (RCLike.I : K) c]36 have hI (x : E) : f ((RCLike.I : K) • x) = (RCLike.I : K) • f x := by37 obtain h | h := @RCLike.I_mul_I_ax K _38 · simp [f, h]39 · simp [f, smul_sub, smul_smul, h, add_comm]40 { toFun := f41 map_add' := hadd42 map_smul' := fun c x => by43 rw [← RCLike.re_add_im c]44 simp only [RingHom.id_apply, add_smul, ← smul_smul, hadd, hreal, hI]45 cont := by dsimp [f]; fun_prop }4647@[simp] theorem scalarLinearPart_apply (A : E →L[ℝ] F) (x : E) :48 scalarLinearPart (K := K) A x = A x - (RCLike.I : K) • A ((RCLike.I : K) • x) := rfl4950variable (K)5152def intervalOfReal : IntervalL1 ℝ →L[ℝ] IntervalL1 K :=53 (@RCLike.ofRealCLM K _).compLpL 1 intervalMeasure5455def intervalRe : IntervalL1 K →L[ℝ] IntervalL1 ℝ :=56 (@RCLike.reCLM K _).compLpL 1 intervalMeasure5758theorem coeFn_intervalOfReal (f : IntervalL1 ℝ) :59 intervalOfReal K f =ᵐ[intervalMeasure] fun x => (f x : K) :=60 (@RCLike.ofRealCLM K _).coeFn_compLpL f6162theorem coeFn_intervalRe (f : IntervalL1 K) :63 intervalRe K f =ᵐ[intervalMeasure] fun x => RCLike.re (f x) :=64 (@RCLike.reCLM K _).coeFn_compLpL f6566@[simp] theorem intervalRe_ofReal (f : IntervalL1 ℝ) :67 intervalRe K (intervalOfReal K f) = f := by68 apply Lp.ext69 filter_upwards [coeFn_intervalRe K (intervalOfReal K f), coeFn_intervalOfReal K f]70 with x hr hf71 simp [hr, hf]7273@[simp] theorem intervalRe_I_ofReal (f : IntervalL1 ℝ) :74 intervalRe K ((RCLike.I : K) • intervalOfReal K f) = 0 := by75 apply Lp.ext76 filter_upwards [coeFn_intervalRe K ((RCLike.I : K) • intervalOfReal K f),77 Lp.coeFn_smul (RCLike.I : K) (intervalOfReal K f), coeFn_intervalOfReal K f,78 Lp.coeFn_zero ℝ 1 intervalMeasure] with x hr hs hf hz79 rw [hr, hs]80 change RCLike.re ((RCLike.I : K) * intervalOfReal K f x) = _81 rw [hf]82 simpa using hz.symm8384theorem intervalOfReal_indicator (n i : ℕ) :85 intervalOfReal K (indicatorConstLp 1 (DyadicTrace.measurableSet_cell n i)86 (measure_ne_top intervalMeasure _) (1 : ℝ)) =87 indicatorConstLp 1 (DyadicTrace.measurableSet_cell n i)88 (measure_ne_top intervalMeasure _) (1 : K) := by89 apply Lp.ext90 filter_upwards [coeFn_intervalOfReal K (indicatorConstLp 191 (DyadicTrace.measurableSet_cell n i) (measure_ne_top intervalMeasure _) (1 : ℝ)),92 indicatorConstLp_coeFn (p := 1) (hs := DyadicTrace.measurableSet_cell n i)93 (hμs := measure_ne_top intervalMeasure _) (c := (1 : ℝ)),94 indicatorConstLp_coeFn (p := 1) (hs := DyadicTrace.measurableSet_cell n i)95 (hμs := measure_ne_top intervalMeasure _) (c := (1 : K))] with x hc hr hk96 rw [hc, hr, hk]97 by_cases hx : x ∈ DyadicTrace.cell n i <;> simp [hx]9899variable {K}100101def extendRealInput (B : IntervalL1 ℝ →L[ℝ] E) : IntervalL1 K →L[K] E :=102 scalarLinearPart (B.comp (intervalRe K))103104def extendRealOutput (A : F →L[ℝ] IntervalL1 ℝ) : F →L[K] IntervalL1 K :=105 scalarLinearPart ((intervalOfReal K).comp A)106107@[simp] theorem extendRealInput_ofReal (B : IntervalL1 ℝ →L[ℝ] E)108 (f : IntervalL1 ℝ) : extendRealInput B (intervalOfReal K f) = B f := by109 simp [extendRealInput]110111@[simp] theorem intervalRe_extendRealOutput (A : F →L[ℝ] IntervalL1 ℝ) (x : F) :112 intervalRe K (extendRealOutput A x) = A x := by113 simp [extendRealOutput]114115theorem trace_real_part (R : IntervalL1 K →L[K] IntervalL1 K) (n : ℕ) :116 DyadicTrace.trace n ((intervalRe K).comp117 ((R.restrictScalars ℝ).comp (intervalOfReal K))) = RCLike.re (DyadicTrace.trace n R) := by118 rw [DyadicTrace.trace_eq, DyadicTrace.trace_eq, map_sum]119 apply Finset.sum_congr rfl120 intro i hi121 simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_restrictScalars',122 intervalOfReal_indicator]123 rw [← integral_re]124 · exact integral_congr_ae (ae_restrict_of_ae (coeFn_intervalRe K _))125 · exact (L1.integrable_coeFn _).integrableOn126127/-- Scalar vanishing trace descends to the underlying real operator. -/128theorem hasVanishingDyadicTrace_restrictScalars (S : E →L[K] F)129 (hS : HasVanishingDyadicTrace S) : HasVanishingDyadicTrace (S.restrictScalars ℝ) := by130 intro A B131 have h := ((@RCLike.reCLM K _).continuous.tendsto 0).comp132 (hS (extendRealOutput A) (extendRealInput B))133 have he : (intervalRe K).comp134 ((((extendRealOutput A).comp (S.comp (extendRealInput B))).restrictScalars ℝ).comp135 (intervalOfReal K)) = A.comp ((S.restrictScalars ℝ).comp B) := by136 ext f137 simp138 rw [map_zero] at h139 change Tendsto (fun n => RCLike.re (DyadicTrace.trace n140 ((extendRealOutput A).comp (S.comp (extendRealInput B))))) atTop (𝓝 0) at h141 simpa only [← trace_real_part, he] using h142143theorem constant_intervalProjection_real_hasVanishingDyadicTrace (K : Type*) [RCLike K] :144 HasVanishingDyadicTrace ((Noise.intervalProjection K Noise.constantRates).restrictScalars ℝ) :=145 hasVanishingDyadicTrace_restrictScalars _146 (Noise.constant_intervalProjection_hasVanishingDyadicTrace K)147148#print axioms hasVanishingDyadicTrace_restrictScalars149150end PL1.ComplementedLattice151