Definitions

The project’s definitions for reading Theorems A and B. Each excerpt is extracted from the frozen Lean source; its source link includes the imports, notation and surrounding parameters.

Lebesgue measure on the interval
The interval space L₁
The sequence space ℓ₂
The sequence space ℓ₁
The projection bound
The underlying real space
Weak convergence of a sequence
The Schur property
A Dunford–Pettis operator
A bounded projection
An isomorphic copy
The Radon–Nikodým property
An equivalent real lattice norm

Lebesgue measure on the interval

Lebesgue measure restricted to the closed interval $[0,1]$ . It is a measure on $\mathbb R$ ; sets outside the interval have measure zero.

Project definition, using Mathlib notions.

PL1/Definitions.lean:31

def intervalMeasure : Measure ℝ := volume.restrict (Set.Icc (0 : ℝ) 1)

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def intervalMeasure : Measure ℝ := volume.restrict (Set.Icc (0 : ℝ) 1)

1 / 2

Name and measure type

def intervalMeasure : Measure ℝ :=

How to read it: def intervalMeasure : Measure ℝ := names a measure on the real line.
Mathematical meaning: The underlying measurable space is the real line with its standard measurable structure.
Role in the statement: This fixes the measure used by every occurrence of the interval function space.

Complete source and context

Restricting Lebesgue measure

volume.restrict (Set.Icc (0 : ℝ) 1)

How to read it: volume is Lebesgue measure. restrict restricts it to Set.Icc (0 : ℝ) 1, the closed interval.
Mathematical meaning: For a measurable set A the measure is the Lebesgue measure of its intersection with [0,1].
Role in the statement: The measure has total mass one; values away from [0,1] do not affect the resulting L₁ classes.

Complete source and context

The interval space L₁

The actual space $L_1([0,1];\mathbb K)$ , with its integral norm and functions identified almost everywhere.

Project abbreviation of Mathlib’s measure-theoretic Lp space.

PL1/Definitions.lean:34

abbrev IntervalL1 (𝕜 : Type*) [RCLike 𝕜] := Lp 𝕜 1 intervalMeasure

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

abbrev IntervalL1 (𝕜 : Type*) [RCLike 𝕜] := Lp 𝕜 1 intervalMeasure

1 / 2

Scalar parameter

abbrev IntervalL1 (𝕜 : Type*) [RCLike 𝕜] :=

How to read it: abbrev introduces a transparent abbreviation. 𝕜 is the scalar type, with the real/complex structure given by [RCLike 𝕜].
Mathematical meaning: The intended specialisations are ℝ and ℂ.
Role in the statement: The same scalar choice is retained in the ambient space, operators and scalar isomorphisms.

Complete source and context

Integrability and the norm

Lp 𝕜 1 intervalMeasure

How to read it: Read Lp 𝕜 1 intervalMeasure as scalar-valued Lp with exponent one for the interval measure.
Mathematical meaning: Elements are almost-everywhere classes of integrable functions; the norm is the integral of the scalar absolute value.
Role in the statement: This is a concrete Mathlib function space, not an abstract space satisfying only selected properties.

intervalMeasure Complete source and context

The sequence space ℓ₂

Scalar sequences $(x_n)_{n\in\mathbb N}$ with $\sum_n |x_n|^2<\infty$ , equipped with $(\sum_n|x_n|^2)^{1/2}$ .

Project abbreviation of Mathlib’s sequence space lp.

PL1/Definitions.lean:37

abbrev Ell2 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 2

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

abbrev Ell2 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 2

1 / 2

A scalar sequence-space abbreviation

abbrev Ell2 (𝕜 : Type*) [RCLike 𝕜] :=

How to read it: abbrev Ell2 names a space for each real/complex scalar type.
Mathematical meaning: The scalar field is the same one appearing in the copy condition.
Role in the statement: This is the model space contained in the range in Theorem B.

Complete source and context

The family and exponent

lp (fun _ : ℕ => 𝕜) 2

How to read it: fun _ : ℕ => 𝕜 is the constant family of scalar coordinate spaces. 2 is the exponent.
Mathematical meaning: All natural-number coordinates, starting at 0, carry the scalar absolute-value norm. The counting sum gives square summability.
Role in the statement: The definition uses the usual infinite sequence space; it imposes no finite support condition.

Complete source and context

The sequence space ℓ₁

Absolutely summable scalar sequences, with norm $\sum_{n\in\mathbb N}|x_n|$ .

Project abbreviation of Mathlib’s sequence space lp; used in the development around the principal results.

PL1/Definitions.lean:40

abbrev Ell1 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 1

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

abbrev Ell1 (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 1

1 / 2

A scalar sequence-space abbreviation

abbrev Ell1 (𝕜 : Type*) [RCLike 𝕜] :=

How to read it: abbrev Ell1 names a space for each real/complex scalar type.
Mathematical meaning: The abbreviation keeps the scalar choice explicit.
Role in the statement: This model occurs in the development and its structural arguments.

Complete source and context

Absolute summability

lp (fun _ : ℕ => 𝕜) 1

How to read it: The family is constant over ℕ; the exponent is 1.
Mathematical meaning: A sequence belongs precisely when the counting sum of its coordinate norms is finite. Its norm is that sum.
Role in the statement: Indexing begins at 0. This sequence space is different from the nonatomic interval L₁ space.

IntervalL1 Complete source and context

The projection bound

The common bound $4+3\sqrt2$ for the norms of the two projections.

Project definition, using Mathlib notions.

PL1/Definitions.lean:43

def projectionBound : ℝ := 4 + 3 * Real.sqrt 2

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def projectionBound : ℝ := 4 + 3 * Real.sqrt 2

1 / 2

A real constant

def projectionBound : ℝ :=

How to read it: def projectionBound : ℝ := declares a real-valued constant.
Mathematical meaning: The value is used in a non-strict operator-norm inequality.
Role in the statement: Both main propositions refer to this identical definition.

Complete source and context

The exact value

4 + 3 * Real.sqrt 2

How to read it: Read the expression as four plus three times the nonnegative square root of two.
Mathematical meaning: The constant is exactly 4 + 3√2.
Role in the statement: The statements establish this bound without claiming it is optimal.

Complete source and context

The underlying real space

The same normed additive group as a $\mathbb K$ -space, with scalar multiplication restricted to $\mathbb R$ . The elements and norm are unchanged.

Project abbreviation of Mathlib’s RestrictScalars.

PL1/Definitions.lean:47

abbrev UnderlyingReal (𝕜 : Type*) [RCLike 𝕜]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :=
  RestrictScalars ℝ 𝕜 E

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

abbrev UnderlyingReal (𝕜 : Type*) [RCLike 𝕜]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :=
  RestrictScalars ℝ 𝕜 E

1 / 2

Space and scalar parameters

abbrev UnderlyingReal (𝕜 : Type*) [RCLike 𝕜]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :=

How to read it: 𝕜 has a real/complex structure. E has a normed additive-group structure and a compatible normed scalar action.
Mathematical meaning: The given mathematical structures in square brackets specify the original space.
Role in the statement: These are parameters of the definition; taking the underlying real space does not choose a different norm.

Complete source and context

Restrict the scalar action

RestrictScalars ℝ 𝕜 E

How to read it: Read this as restricting the scalar action on E from 𝕜 to ℝ.
Mathematical meaning: Real numbers act through their canonical inclusion in the real/complex scalar field.
Role in the statement: The instance immediately following the abbreviation in the complete source registers this action. The main propositions pass it explicitly in their last clauses.

Complete source and context

Weak convergence of a sequence

A sequence $x_n$ converges weakly to $a$ when $\varphi(x_n)\to\varphi(a)$ for every continuous scalar-linear functional $\varphi$ .

Project definition, using Mathlib notions.

PL1/Definitions.lean:64

def WeaklyConverges (x : ℕ → E) (a : E) : Prop :=
  ∀ φ : E →L[𝕜] 𝕜, Tendsto (fun n => φ (x n)) atTop (𝓝 (φ a))

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def WeaklyConverges (x : ℕ → E) (a : E) : Prop :=
  ∀ φ : E →L[𝕜] 𝕜, Tendsto (fun n => φ (x n)) atTop (𝓝 (φ a))

1 / 3

The sequence and its limit

def WeaklyConverges (x : ℕ → E) (a : E) : Prop :=

How to read it: x : ℕ → E is a sequence; a : E is a proposed limit. : Prop makes this a proposition.
Mathematical meaning: The scalar field and space come from the section parameters shown alongside the definition.
Role in the statement: The limit is part of the claim and is kept fixed for every functional.

Complete source and context

The entire continuous dual

∀ φ : E →L[𝕜] 𝕜,

How to read it: ∀ means “for every”. The type E →L[𝕜] 𝕜 consists of continuous scalar-linear functionals.
Mathematical meaning: The condition tests against every member of the continuous dual, not merely coordinate functionals.
Role in the statement: This is what makes the convergence weak convergence over the chosen field.

Complete source and context

Convergence of each scalar sequence

Tendsto (fun n => φ (x n)) atTop (𝓝 (φ a))

How to read it: fun n => φ (x n) applies the functional to each term. atTop means as n tends to infinity; 𝓝 (φ a) is the neighbourhood filter of φ(a).
Mathematical meaning: For each functional, its values converge to its value at the same a.
Role in the statement: This scalar convergence completes the definition; no convergence in the norm of E is required here.

Complete source and context

The Schur property

Every weakly convergent sequence in $E$ converges to the same limit in the given norm.

Project definition, using Mathlib notions.

PL1/Definitions.lean:68

def HasSchurProperty : Prop :=
  ∀ (x : ℕ → E) (a : E),
    WeaklyConverges 𝕜 E x a → Tendsto x atTop (𝓝 a)

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def HasSchurProperty : Prop :=
  ∀ (x : ℕ → E) (a : E),
    WeaklyConverges 𝕜 E x a → Tendsto x atTop (𝓝 a)

1 / 3

Name of the property

def HasSchurProperty : Prop :=

How to read it: def HasSchurProperty : Prop := names a claim about the scalar field and space fixed in the section.
Mathematical meaning: This is a property of that particular normed space.
Role in the statement: It is used positively for the range in A and negatively for the range in B.

Complete source and context

All sequences and limits

∀ (x : ℕ → E) (a : E),

How to read it: The universal quantifiers range over every sequence and every candidate limit in E.
Mathematical meaning: There is no additional boundedness premise or special class of sequences.
Role in the statement: The implication below must hold for all these choices.

Complete source and context

Weak convergence implies norm convergence

WeaklyConverges 𝕜 E x a → Tendsto x atTop (𝓝 a)

How to read it: → is implication. The premise is weak convergence; Tendsto x atTop (𝓝 a) is convergence in the topology of E.
Mathematical meaning: The topology here is induced by E’s given norm, so x converges to a in norm.
Role in the statement: This equivalent all-limits formulation includes the weakly null formulation in the paper.

WeaklyConverges Complete source and context

A Dunford–Pettis operator

A bounded linear operator $T:E\to F$ that sends weakly convergent sequences to norm-convergent sequences with the corresponding image limit.

Project definition, using Mathlib notions.

The enclosing section fixes (𝕜 : Type*) [RCLike 𝕜] and (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]. These parameters are retained in the declaration; follow the source link to read their exact context. The section also fixes a normed 𝕜-space F; {𝕜 E} makes the indicated parameters implicit for this declaration.

PL1/Definitions.lean:78

def IsDunfordPettis (T : E →L[𝕜] F) : Prop :=
  ∀ (x : ℕ → E) (a : E),
    WeaklyConverges 𝕜 E x a →
      Tendsto (fun n => T (x n)) atTop (𝓝 (T a))

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def IsDunfordPettis (T : E →L[𝕜] F) : Prop :=
  ∀ (x : ℕ → E) (a : E),
    WeaklyConverges 𝕜 E x a →
      Tendsto (fun n => T (x n)) atTop (𝓝 (T a))

1 / 4

The bounded linear map

def IsDunfordPettis (T : E →L[𝕜] F) : Prop :=

How to read it: T : E →L[𝕜] F is a continuous scalar-linear map, equivalently a bounded linear operator in this setting.
Mathematical meaning: Its domain and codomain use the field and normed-space structures from the section.
Role in the statement: The property is attached to this operator; boundedness is already in its type.

Complete source and context

Every sequence and limit in the domain

∀ (x : ℕ → E) (a : E),

How to read it: The quantifiers range over sequences in E and possible limits in E.
Mathematical meaning: One operator must satisfy the condition for every such choice.
Role in the statement: No restriction to a chosen family of functions is made.

Complete source and context

The weak convergence premise

WeaklyConverges 𝕜 E x a →

How to read it: Read the implication as “if x converges weakly to a, then …”.
Mathematical meaning: Weak convergence is tested against the whole continuous dual of the domain.
Role in the statement: This is the hypothesis on the sequence.

WeaklyConverges Complete source and context

Norm convergence in the codomain

Tendsto (fun n => T (x n)) atTop (𝓝 (T a))

How to read it: The sequence is T (x n) and its limit is T a; 𝓝 uses the norm topology of F.
Mathematical meaning: The images converge in the codomain norm.
Role in the statement: By subtracting the limit this is equivalent to carrying weakly null sequences to norm-null sequences, as in the paper.

Complete source and context

A bounded projection

A bounded linear operator $P:E\to E$ with $P^2=P$ .

Project definition, using Mathlib notions.

PL1/Definitions.lean:84

def IsProjection (P : E →L[𝕜] E) : Prop := P.comp P = P

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def IsProjection (P : E →L[𝕜] E) : Prop := P.comp P = P

1 / 2

An operator on one space

def IsProjection (P : E →L[𝕜] E) : Prop :=

How to read it: P : E →L[𝕜] E has the same domain and codomain. : Prop makes the definition a claim about it.
Mathematical meaning: P is already bounded and linear by its type.
Role in the statement: The equation that follows adds idempotence.

Complete source and context

Idempotence

P.comp P = P

How to read it: P.comp P is composition of P with itself.
Mathematical meaning: Applying P twice has the same effect as applying it once.
Role in the statement: The range is the projected subspace; in the main statements its norm is inherited from the ambient L₁ space.

Complete source and context

An isomorphic copy

A closed subspace $V$ of $E$ together with a bounded scalar-linear isomorphism $D\to V$ whose inverse is bounded.

Project definition, using Mathlib notions.

PL1/Definitions.lean:91

def ContainsIsomorphicCopy (𝕜 : Type*) [RCLike 𝕜]
    (D : Type*) [NormedAddCommGroup D] [NormedSpace 𝕜 D]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=
  ∃ V : Submodule 𝕜 E,
    IsClosed (V : Set E) ∧ Nonempty (D ≃L[𝕜] V)

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def ContainsIsomorphicCopy (𝕜 : Type*) [RCLike 𝕜]
    (D : Type*) [NormedAddCommGroup D] [NormedSpace 𝕜 D]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=
  ∃ V : Submodule 𝕜 E,
    IsClosed (V : Set E) ∧ Nonempty (D ≃L[𝕜] V)

1 / 4

The scalar field and two spaces

def ContainsIsomorphicCopy (𝕜 : Type*) [RCLike 𝕜]
    (D : Type*) [NormedAddCommGroup D] [NormedSpace 𝕜 D]
    (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=

How to read it: The binders fix a scalar type 𝕜 and normed 𝕜-spaces D and E.
Mathematical meaning: D is the model to be copied; E is the containing space.
Role in the statement: The two spaces have their own given norms. The order of parameters matters.

Complete source and context

Choose the subspace

∃ V : Submodule 𝕜 E,

How to read it: ∃ means “there exists”; Submodule 𝕜 E is a scalar-linear subspace of E.
Mathematical meaning: One subspace V is chosen inside E.
Role in the statement: The later closedness and equivalence conditions refer to this same V.

Complete source and context

Closedness in the ambient norm

IsClosed (V : Set E) ∧

How to read it: The coercion (V : Set E) regards the subspace as a set. ∧ joins this condition to the next.
Mathematical meaning: The subspace is closed in the norm topology of E and uses the inherited norm.
Role in the statement: Closure is part of the definition, so a merely algebraic copy does not suffice.

Complete source and context

An isomorphism with bounded inverse

Nonempty (D ≃L[𝕜] V)

How to read it: ≃L[𝕜] is a continuous linear equivalence; Nonempty means at least one such equivalence exists.
Mathematical meaning: There is a bounded bijective scalar-linear map from D onto V with bounded inverse.
Role in the statement: This is stronger than the bare existence of an injective continuous linear map. Negating the predicate excludes all admissible V and all these equivalences.

Complete source and context

The Radon–Nikodým property

Every absolutely continuous, countably additive $E$ -valued vector measure of finite variation on a finite measure space has a Bochner-integrable density.

Project vector-measure definition, using Mathlib’s VectorMeasure, variation and Bochner integral.

PL1/Definitions.lean:108

def HasRadonNikodymProperty (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=
  ∀ (Ω : Type v) (mΩ : MeasurableSpace Ω),
    letI := mΩ
    ∀ μ : Measure Ω, μ Set.univ < ∞ →
      ∀ ν : VectorMeasure Ω E, ν.variation Set.univ < ∞ →
        (∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) →
          ∃ g : Ω → E, Integrable g μ ∧
            ∀ A : Set Ω, MeasurableSet A → ν A = ∫ x in A, g x ∂μ

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def HasRadonNikodymProperty (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=
  ∀ (Ω : Type v) (mΩ : MeasurableSpace Ω),
    letI := mΩ
    ∀ μ : Measure Ω, μ Set.univ < ∞ →
      ∀ ν : VectorMeasure Ω E, ν.variation Set.univ < ∞ →
        (∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) →
          ∃ g : Ω → E, Integrable g μ ∧
            ∀ A : Set Ω, MeasurableSet A → ν A = ∫ x in A, g x ∂μ

1 / 8

A real normed target space

def HasRadonNikodymProperty (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=

How to read it: The binders fix E : Type u, its normed additive group, and its real normed scalar action.
Mathematical meaning: Bochner integration is taken in the real normed target. A complex range is viewed through its underlying real space.
Role in the statement: This is the full vector-measure property, not a substitute based on one operator.

UnderlyingReal Complete source and context

Every measurable source space

∀ (Ω : Type v) (mΩ : MeasurableSpace Ω),

How to read it: The universal quantifiers choose an underlying type Ω and a measurable-space structure on it. Type v specifies the universe in which Ω ranges.
Mathematical meaning: The definition permits an independent universe v for the source space.
Role in the statement: The main Theorem A proposition explicitly specialises v to 0, separately from the universe of its target.

Complete source and context

Use the chosen measurable sets

letI := mΩ

How to read it: letI installs mΩ as the measurable structure for the remaining expression.
Mathematical meaning: All subsequent measures and measurable sets refer to this same choice.
Role in the statement: This binds the meaning of measurability throughout the density statement.

Complete source and context

Every finite scalar measure

∀ μ : Measure Ω, μ Set.univ < ∞ →

How to read it: For every measure μ, the implication assumes its value on the whole space is less than infinity.
Mathematical meaning: μ is a finite nonnegative measure; it need not be a probability measure. Measure values lie in the extended nonnegative reals [0, ∞]; the displayed inequality excludes infinite total mass.
Role in the statement: The finiteness bound is an assumption restricting the measures for which a density is required.

Complete source and context

Every vector measure of finite variation

∀ ν : VectorMeasure Ω E, ν.variation Set.univ < ∞ →

How to read it: ν is a Mathlib countably additive E-valued vector measure. Its total variation on the whole space is required to be finite.
Mathematical meaning: The vector measure must have bounded total variation.
Role in the statement: This is a second restriction on the measures under consideration, not a conclusion about arbitrary vector measures.

Complete source and context

Absolute continuity

(∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) →

How to read it: For every measurable A, if μ(A)=0 then ν(A)=0; the outer implication uses this complete condition as a premise.
Mathematical meaning: The vector measure vanishes on μ-null measurable sets.
Role in the statement: Together with the two finiteness conditions, this is the admissibility condition for the density conclusion.

Complete source and context

One integrable density

∃ g : Ω → E, Integrable g μ ∧

How to read it: There exists a function g from Ω to E that is Bochner integrable for μ. ∧ also requires the identity below.
Mathematical meaning: The density may depend on the space, μ and ν.
Role in the statement: One g must represent ν on every measurable set, rather than choosing a new g for each set.

Complete source and context

Represent every measurable set

∀ A : Set Ω, MeasurableSet A → ν A = ∫ x in A, g x ∂μ

How to read it: For all measurable A, ν(A) equals the set integral of g with respect to μ.
Mathematical meaning: The same density integrates to the vector measure on every measurable set.
Role in the statement: This completes the RNP definition. Negating it, as in A, denies the universal density property.

Complete source and context

An equivalent real lattice norm

A compatible real vector-lattice order on $E$ and a solid norm equivalent to its original norm. Both the lattice order and the norm may vary.

Project definition, using Mathlib lattice orders and seminorms. Its Banach-lattice bridge uses the separately attributed BanLat library.

PL1/LatticeDefinitions.lean:26

def HasEquivalentRealLatticeNorm (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=
  ∃ latticeOrder : Lattice E,
    letI := latticeOrder
    IsOrderedAddMonoid E ∧ PosSMulMono ℝ E ∧
      ∃ p : Seminorm ℝ E,
        (∀ x y : E, |x| ≤ |y| → p x ≤ p y) ∧
        ∃ a b : ℝ, 0 < a ∧ 0 < b ∧
          ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖

Explain this Lean definition

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def HasEquivalentRealLatticeNorm (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=
  ∃ latticeOrder : Lattice E,
    letI := latticeOrder
    IsOrderedAddMonoid E ∧ PosSMulMono ℝ E ∧
      ∃ p : Seminorm ℝ E,
        (∀ x y : E, |x| ≤ |y| → p x ≤ p y) ∧
        ∃ a b : ℝ, 0 < a ∧ 0 < b ∧
          ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖

1 / 8

The existing real normed space

def HasEquivalentRealLatticeNorm (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=

How to read it: The binders fix a normed additive group E with a real normed scalar action.
Mathematical meaning: The original addition, real scalar multiplication and norm are the reference structures.
Role in the statement: The definition will vary the lattice order and the new norm while retaining the given vector space.

Complete source and context

An arbitrary lattice order

∃ latticeOrder : Lattice E,

How to read it: There exists a Lattice E, giving an order with joins and meets of each pair.
Mathematical meaning: The order is chosen as part of the claim.
Role in the statement: The negative main-theorem clause rules out every order satisfying the remaining compatibility and equivalent-solid-norm conditions. It does not prohibit bare lattice orders on the underlying set.

Complete source and context

Use that order

letI := latticeOrder

How to read it: The local instance makes the chosen lattice order active in the remaining expression.
Mathematical meaning: The inequalities and lattice absolute values below are interpreted using this chosen order.
Role in the statement: All later order conditions concern the same lattice.

Complete source and context

Compatibility with vector addition and real scalars

IsOrderedAddMonoid E ∧ PosSMulMono ℝ E ∧

How to read it: IsOrderedAddMonoid expresses compatibility with addition; PosSMulMono ℝ E expresses monotonicity under nonnegative real scalar multiplication.
Mathematical meaning: Together with the existing real vector space and lattice, these give a real vector-lattice structure.
Role in the statement: A bare lattice on the set would not suffice. Both compatibility conditions are required.

Complete source and context

A candidate lattice norm

∃ p : Seminorm ℝ E,

How to read it: Choose a real seminorm p on the existing vector space.
Mathematical meaning: A seminorm is subadditive and absolutely homogeneous. It may initially vanish at a nonzero vector.
Role in the statement: The positive lower bound imposed later forces p to be a genuine norm.

Complete source and context

Solidity

(∀ x y : E, |x| ≤ |y| → p x ≤ p y) ∧

How to read it: For all x and y, if their lattice absolute values satisfy |x| ≤ |y|, then p(x) ≤ p(y).
Mathematical meaning: The candidate norm is monotone with respect to the lattice modulus.
Role in the statement: This is the lattice-norm compatibility condition; the absolute values here are lattice operations.

Complete source and context

Two positive comparison constants

∃ a b : ℝ, 0 < a ∧ 0 < b ∧

How to read it: There exist real a and b, both strictly positive.
Mathematical meaning: These constants are chosen once for the whole space.
Role in the statement: Positivity is required even for the zero space; no exception is inserted into the definition.

Complete source and context

Equivalence of norms

∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖

How to read it: For every x, a times the original norm is at most p(x), and p(x) is at most b times the original norm.
Mathematical meaning: The two bounds make p equivalent to the original norm and ensure p(x)>0 when x≠0. On a complete E, the equivalent norm is complete.
Role in the statement: The BanLat bridge in PL1/LatticeBridge.lean proves the implication from a bounded real-linear isomorphism to a BanLat Banach lattice. The main negation excludes even renorming, not just compatibility with the inherited norm.

Complete source and context