PL1/ComplementedLatticeRealAmbient.lean
All source files · Download exact source
SHA-256: 416f399303f7c9ae872ae4ef4256a89b241b50dc3dd6a125e4ff29a8adc017b9
1import PL1.ComplementedLatticeReduction23/-! # A concrete real interval ambient space for the scalar construction45The real and imaginary parts embed scalar L1 into the first two coordinates6of a real L1 sum. The existing probability sampler and averaging retraction7then place that sum complementably in real interval L1.8-/910noncomputable section11set_option backward.isDefEq.respectTransparency false12open MeasureTheory13open scoped ENNReal1415namespace PL1.ComplementedLattice1617open EnfloStarbird18attribute [local instance] DyadicTrace.intervalMeasure_probability1920variable (K : Type*) [RCLike K]2122def intervalIm : IntervalL1 K →L[ℝ] IntervalL1 ℝ :=23 (@RCLike.imCLM K _).compLpL 1 intervalMeasure2425theorem coeFn_intervalIm (f : IntervalL1 K) :26 intervalIm K f =ᵐ[intervalMeasure] fun x => RCLike.im (f x) :=27 (@RCLike.imCLM K _).coeFn_compLpL f2829theorem interval_re_add_im (f : IntervalL1 K) :30 intervalOfReal K (intervalRe K f) + (RCLike.I : K) • intervalOfReal K (intervalIm K f) = f := by31 apply Lp.ext32 filter_upwards [Lp.coeFn_add (intervalOfReal K (intervalRe K f))33 ((RCLike.I : K) • intervalOfReal K (intervalIm K f)),34 Lp.coeFn_smul (RCLike.I : K) (intervalOfReal K (intervalIm K f)),35 coeFn_intervalOfReal K (intervalRe K f), coeFn_intervalOfReal K (intervalIm K f),36 coeFn_intervalRe K f, coeFn_intervalIm K f] with x ha hs hor hoi hr hi37 rw [ha]38 change intervalOfReal K (intervalRe K f) x +39 ((RCLike.I : K) • intervalOfReal K (intervalIm K f)) x = f x40 rw [hs, hor]41 change (intervalRe K f x : K) + (RCLike.I : K) * intervalOfReal K (intervalIm K f) x = _42 rw [hoi, hr, hi, mul_comm RCLike.I, RCLike.re_add_im]4344def realCoordinateEmbedding : IntervalL1 K →L[ℝ] L1Sum (IntervalL1 ℝ) :=45 (lp.singleContinuousLinearMap ℝ (fun _ : ℕ => IntervalL1 ℝ) 1 0).comp (intervalRe K) +46 (lp.singleContinuousLinearMap ℝ (fun _ : ℕ => IntervalL1 ℝ) 1 1).comp (intervalIm K)4748def realCoordinateRetraction : L1Sum (IntervalL1 ℝ) →L[ℝ] IntervalL1 K :=49 (intervalOfReal K).comp (lp.evalCLM ℝ (fun _ : ℕ => IntervalL1 ℝ) 1 0) +50 (RCLike.I : K) • (intervalOfReal K).comp (lp.evalCLM ℝ (fun _ : ℕ => IntervalL1 ℝ) 1 1)5152theorem realCoordinateRetraction_embedding (f : IntervalL1 K) :53 realCoordinateRetraction K (realCoordinateEmbedding K f) = f := by54 simpa [realCoordinateRetraction, realCoordinateEmbedding, lp.evalCLM, lp.evalₗ,55 lp.single_apply] using interval_re_add_im K f5657def realCoordinateCopy : ComplementedCopy ℝ (IntervalL1 K) (L1Sum (IntervalL1 ℝ)) :=58 ⟨realCoordinateEmbedding K, realCoordinateRetraction K, realCoordinateRetraction_embedding K⟩5960def realSumIntervalEmbedding : L1Sum (IntervalL1 ℝ) →L[ℝ] IntervalL1 ℝ :=61 (IntervalSubtype.equiv ℝ).toContinuousLinearEquiv.toContinuousLinearMap.comp62 ((IntervalRetraction.pullback (IntervalModel.probabilityMeasure intervalMeasure)).toContinuousLinearMap.comp63 (IntervalModel.sumProbabilityEquiv (𝕜 := ℝ) intervalMeasure).toContinuousLinearEquiv.toContinuousLinearMap)6465def realSumIntervalRetraction : IntervalL1 ℝ →L[ℝ] L1Sum (IntervalL1 ℝ) :=66 (IntervalModel.sumProbabilityEquiv (𝕜 := ℝ) intervalMeasure).symm.toContinuousLinearEquiv.toContinuousLinearMap.comp67 ((IntervalRetraction.retraction (IntervalModel.probabilityMeasure intervalMeasure)).comp68 (IntervalSubtype.equiv ℝ).symm.toContinuousLinearEquiv.toContinuousLinearMap)6970theorem realSumIntervalRetraction_embedding (f : L1Sum (IntervalL1 ℝ)) :71 realSumIntervalRetraction (realSumIntervalEmbedding f) = f := by72 simp [realSumIntervalRetraction, realSumIntervalEmbedding]7374def realSumIntervalCopy : ComplementedCopy ℝ (L1Sum (IntervalL1 ℝ)) (IntervalL1 ℝ) :=75 ⟨realSumIntervalEmbedding, realSumIntervalRetraction, realSumIntervalRetraction_embedding⟩7677def complementedCopyComp {D E F : Type*}78 [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E]79 [NormedAddCommGroup F] [NormedSpace ℝ F]80 (C : ComplementedCopy ℝ D E) (B : ComplementedCopy ℝ E F) : ComplementedCopy ℝ D F where81 embedding := B.embedding.comp C.embedding82 retraction := C.retraction.comp B.retraction83 left_inv := fun x => (congrArg C.retraction (B.left_inv (C.embedding x))).trans (C.left_inv x)8485/-- Every real or complex interval L1 in this construction embeds complementably86in the actual real interval L1, using its natural compatible real scalar action. -/87def scalarIntervalRealCopy : ComplementedCopy ℝ (IntervalL1 K) (IntervalL1 ℝ) :=88 complementedCopyComp (realCoordinateCopy K) realSumIntervalCopy8990/-- The same conclusion with the explicit restricted scalar convention. -/91def underlyingIntervalRealCopy :92 ComplementedCopy ℝ (UnderlyingReal K (IntervalL1 K)) (IntervalL1 ℝ) :=93 complementedCopyTransport (scalarIntervalRealCopy K) (naturalToUnderlyingReal (K := K) (IntervalL1 K))9495#print axioms scalarIntervalRealCopy9697/-- Only the ordinary real complemented-L1 classification is needed, even for98the complex projection. The reduction uses the actual ambient maps above. -/99theorem classification_of_real (K : Type) [RCLike K]100 (h : ComplementedL1LatticeClassification ℝ) : ComplementedL1LatticeClassification K := by101 intro F _ _ _ _ _ hC102 obtain ⟨C⟩ := hC103 exact h F ⟨complementedCopyComp C (scalarIntervalRealCopy K)⟩104105/-- Likewise only real arbitrary-copy extraction in real interval L1 is needed. -/106theorem extraction_of_real (K : Type) [RCLike K]107 (h : L1CopyExtraction ℝ) : L1CopyExtraction K := by108 intro E _ _ _ _ hC hc109 obtain ⟨C⟩ := hC110 exact h E ⟨complementedCopyComp C (scalarIntervalRealCopy K)⟩ hc111112/-- The full reviewed scalar target follows from three standard real structural113inputs; all complex/underlying-real and actual-operator bridges are proved. -/114theorem theoremB_of_real_structural_properties (K : Type) [RCLike K]115 (hclass : ComplementedL1LatticeClassification ℝ)116 (hdich : SeparableRealL1Dichotomy.{0}) (hextract : L1CopyExtraction ℝ) :117 TheoremBStatement K :=118 theoremB_of_structural_properties K (classification_of_real K hclass) hdich119 (extraction_of_real K hextract)120121theorem theoremB_real_and_complex_of_real_structural_properties122 (hclass : ComplementedL1LatticeClassification ℝ)123 (hdich : SeparableRealL1Dichotomy.{0}) (hextract : L1CopyExtraction ℝ) :124 TheoremBRealStatement ∧ TheoremBComplexStrongStatement :=125 ⟨theoremB_of_real_structural_properties ℝ hclass hdich hextract,126 theoremB_of_real_structural_properties ℂ hclass hdich hextract⟩127128#print axioms theoremB_real_and_complex_of_real_structural_properties129130end PL1.ComplementedLattice131