PL1/Definitions.lean

All source files · Download exact source

SHA-256: 1b56c4f85eba48b6cbde93d8cb7674cda5c7227e8671fe2618f7b2dc1020d5f4

1import PL1.LatticeDefinitions2import Mathlib.Analysis.Normed.Lp.lpSpace3import Mathlib.Analysis.RCLike.Basic4import Mathlib.MeasureTheory.Function.LpSpace.Basic5import Mathlib.MeasureTheory.Measure.Lebesgue.Basic6import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic7import Mathlib.MeasureTheory.Integral.Bochner.Basic8import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent9import Mathlib.LinearAlgebra.FiniteDimensional.Defs1011/-!12# Definitions for Theorems A and B of the updated PL1 paper1314All function and sequence spaces are standard Mathlib Lp/lp spaces. No abstract15placeholder substitutes for the actual interval L1, continuous dual, range, or16bounded inverse. RNP is given its vector-measure definition, not replaced by a17single representability test or the Schur property.18-/1920noncomputable section21universe u v w2223open Filter MeasureTheory Module24open scoped Topology ENNReal2526namespace PL12728/-- Lebesgue measure restricted to [0,1]. Outside values are ignored modulo a.e.29equality. Mathlib's a.e.-strongly-measurable Lp construction also accommodates30completed-measure representatives. -/31def intervalMeasure : Measure ℝ := volume.restrict (Set.Icc (0 : ℝ) 1)3233/-- Genuine interval L1 with its integral norm. -/34abbrev IntervalL1 (𝕜 : Type*) [RCLike 𝕜] := Lp 𝕜 1 intervalMeasure3536/-- Standard scalar square-summable sequence space over ℕ. -/37abbrev Ell2 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 23839/-- Standard scalar absolutely summable sequence space over ℕ. -/40abbrev Ell1 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 14142/-- Updated bound claimed in both main theorems; no optimality is asserted. -/43def projectionBound : ℝ := 4 + 3 * Real.sqrt 24445/-- The same normed additive group with its scalar action restricted to ℝ.46This makes every use of the underlying real space explicit. -/47abbrev UnderlyingReal (𝕜 : Type*) [RCLike 𝕜]48    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :=49  RestrictScalars ℝ 𝕜 E5051/-- Register scalar restriction on the explicit type alias. This uses the52original norm and restricts only the scalar action. -/53instance underlyingRealNormedSpace (𝕜 : Type*) [RCLike 𝕜]54    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :55    NormedSpace ℝ (UnderlyingReal 𝕜 E) :=56  NormedSpace.restrictScalars ℝ 𝕜 E5758section WeakConvergence5960variable (𝕜 : Type*) [RCLike 𝕜]61variable (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]6263/-- Weak convergence tested against the entire continuous dual over 𝕜. -/64def WeaklyConverges (x : ℕ → E) (a : E) : Prop :=65  ∀ φ : E →L[𝕜] 𝕜, Tendsto (fun n => φ (x n)) atTop (𝓝 (φ a))6667/-- Weak sequential convergence implies convergence in the given norm. -/68def HasSchurProperty : Prop :=69  ∀ (x : ℕ → E) (a : E),70    WeaklyConverges 𝕜 E x a → Tendsto x atTop (𝓝 a)7172variable {𝕜 E}73variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]7475/-- Dunford–Pettis OPERATOR, or completely continuous operator.76The all-convergent-sequences formulation is equivalent to the weak-null77formulation in the paper, by subtracting the limit. -/78def IsDunfordPettis (T : E →L[𝕜] F) : Prop :=79  ∀ (x : ℕ → E) (a : E),80    WeaklyConverges 𝕜 E x a →81      Tendsto (fun n => T (x n)) atTop (𝓝 (T a))8283/-- Boundedness is already contained in the continuous-linear-map type. -/84def IsProjection (P : E →L[𝕜] E) : Prop := P.comp P = P8586end WeakConvergence8788/-- An isomorphic copy is a closed subspace and a bounded linear equivalence89onto it with bounded inverse. An injective continuous linear map alone would90not express this condition. -/91def ContainsIsomorphicCopy (𝕜 : Type*) [RCLike 𝕜]92    (D : Type*) [NormedAddCommGroup D] [NormedSpace 𝕜 D]93    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=94  ∃ V : Submodule 𝕜 E,95    IsClosed (V : Set E) ∧ Nonempty (D ≃L[𝕜] V)9697/-- The standard vector-measure Radon–Nikodym property.9899For EVERY finite measure space and EVERY countably additive vector measure of100finite total variation vanishing on measure-zero measurable sets, there is a101Bochner-integrable density giving its value on every measurable set.102103The source measurable spaces range over Type v; this universe is independent104of the target space's universe. It is explicit in statement inspection.105The property uses the underlying real scalar action, as does Bochner integration;106the same definition applies to the underlying real space of a complex space.107-/108def HasRadonNikodymProperty (E : Type u) [NormedAddCommGroup E]109    [NormedSpace ℝ E] : Prop :=110  ∀ (Ω : Type v) (mΩ : MeasurableSpace Ω),111    letI := mΩ112    ∀ μ : Measure Ω, μ Set.univ < ∞ →113      ∀ ν : VectorMeasure Ω E, ν.variation Set.univ < ∞ →114        (∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) →115          ∃ g : Ω → E, Integrable g μ ∧116            ∀ A : Set Ω, MeasurableSet A → ν A = ∫ x in A, g x ∂μ117118end PL1119