PL1/ScalarUnconditionalRNP.lean

All source files · Download exact source

SHA-256: 1715b6571b061cc778cb213d68f031de0a1f96d0a3aa098fe694badafb6ae428

1import PL1.UnconditionalRNP2import PL1.ScalarDecompositionRNP3import PL1.RealSchur4import PL1.IntrinsicNonBoundedComplete56/-! # Unconditional sign bounds and RNP over real or complex scalars -/78noncomputable section9universe u v10open Filter11open scoped Topology BigOperators1213namespace PL1.ScalarUnconditionalRNP1415variable {K : Type*} [RCLike K]16variable {E : Type u} [NormedAddCommGroup E] [NormedSpace K E]1718def difference (P : ℕ → E →L[K] E) : ℕ → E →L[K] E19  | 0 => P 020  | n + 1 => P (n + 1) - P n2122theorem hasRNP_of_schur_sign_bound [CompleteSpace E]23    (hS : HasSchurProperty K E) (P : ℕ → E →L[K] E)24    (hfinite : ∀ n, FiniteDimensional K (P n).range)25    (hnested : ∀ m n, m ≤ n → (P m).comp (P n) = P m)26    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x))27    (C : ℝ) (hC : 0 ≤ C)28    (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),29      (∀ j, ε j = 1 ∨ ε j = -1) →30        ‖∑ j ∈ Finset.range (N + 1), (ε j : K) • difference P j y‖ ≤ C * ‖y‖) :31    @HasRadonNikodymProperty.{u, v} (UnderlyingReal K E)32      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ K E) := by33  let := NormedSpace.restrictScalars ℝ K E34  let := IsScalarTower.restrictScalars ℝ K E35  change HasRadonNikodymProperty.{u, v} E36  let Q : ℕ → E →L[ℝ] E := fun n => (P n).restrictScalars ℝ37  have hfiniteR (n : ℕ) : FiniteDimensional ℝ (Q n).range := by38    let := hfinite n39    let : FiniteDimensional ℝ (P n).range := FiniteDimensional.trans ℝ K (P n).range40    exact inferInstanceAs (FiniteDimensional ℝ (P n).range)41  have hd (j : ℕ) (y : E) : UnconditionalDecomposition.difference Q j y = difference P j y := by42    cases j <;> rfl43  refine UnconditionalRNP.hasRadonNikodymProperty_of_schur_unconditional_projections44    (hasSchurProperty_iff_real.mp hS) Q hfiniteR ?_ hstrong C hC ?_45  · intro m n hmn46    ext1 x47    exact DFunLike.congr_fun (hnested m n hmn) x48  · intro N ε y hε49    simpa only [hd, RCLike.real_smul_eq_coe_smul (K := K)] using htransform N ε y hε5051theorem no_uniform_sign_bound_of_not_RNP [CompleteSpace E]52    (hS : HasSchurProperty K E)53    (hRNP : ¬ @HasRadonNikodymProperty.{u, v} (UnderlyingReal K E)54      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ K E))55    (P : ℕ → E →L[K] E) (hfinite : ∀ n, FiniteDimensional K (P n).range)56    (hnested : ∀ m n, m ≤ n → (P m).comp (P n) = P m)57    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x)) :58    ¬ ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),59      (∀ j, ε j = 1 ∨ ε j = -1) →60        ‖∑ j ∈ Finset.range (N + 1), (ε j : K) • difference P j y‖ ≤ C * ‖y‖ := by61  rintro ⟨C, hC, htransform⟩62  exact hRNP (hasRNP_of_schur_sign_bound hS P hfinite hnested hstrong C hC htransform)6364end PL1.ScalarUnconditionalRNP6566namespace PL1.Noise6768theorem schur_intrinsic_no_uniform_scalar_sign_bound (K : Type*) [RCLike K] :69    ¬ ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (ε : ℕ → ℝ)70      (y : (dyadicSystem K schurRates).IntrinsicSpace),71      (∀ j, ε j = 1 ∨ ε j = -1) →72        ‖∑ j ∈ Finset.range (N + 1), (ε j : K) •73          ScalarUnconditionalRNP.difference (intrinsicExpectation K schurRates) j y‖ ≤ C * ‖y‖ :=74  ScalarUnconditionalRNP.no_uniform_sign_bound_of_not_RNP75    (schurRates_intrinsic_hasSchurProperty K) (schur_intrinsic_not_RNP K)76    (intrinsicExpectation K schurRates) (intrinsicExpectation_range_finiteDimensional K schurRates)77    (intrinsicExpectation_comp_of_le K schurRates) (tendsto_intrinsicExpectation K schurRates)7879end PL1.Noise80