Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Time oscillations defeat compactness without derivative control

Statement

Let (V,H,J) be a Banach evolution triple, let T>0, and fix 0≠v∈V. For each positive integer n, define un(t)=sin⁡(2πnt/T) v. Then (un) is bounded in Lp(0,T;V) for every 1≤p<∞, but it has no strongly convergent subsequence in L2(0,T;H). Its time-derivative norm grows linearly in n in every Lq(0,T;V∗), 1≤q≤∞.

Facts & Assumptions

Given: The evolution triple, T>0, 0≠v∈V, and the family defined in the statement.

[F1]

The canonical embedding i:V→H is injective, and J(iv) acts on w∈V by (iv,iw)H (Banach evolution triples and weak time derivatives).

Proof

1.1givenalgebra

Since each interval [0,T] contains exactly n periods of sin⁡(2πnt/T), a change of variable gives ∥un∥Lp(0,T;V)p=∥v∥VpT2π∫02π∣sin⁡s∣p ds, independent of n. Thus the family is uniformly bounded in each stated Lp(V).

1.2F1givenalgebra

For distinct positive integers n≠m, sine orthogonality over [0,T] gives ∥un−um∥L2(0,T;H)2=∥iv∥H2∫0T(sin⁡(2πnt/T)−sin⁡(2πmt/T))2 dt=T∥iv∥H2>0, where positivity follows from injectivity in [F1]. Every two distinct members therefore stay a fixed positive distance apart, so no subsequence is Cauchy and none converges strongly in the complete space L2(0,T;H).

2.1F1step 1.1givenalgebra∎

Scalar integration by parts against each w∈V shows that the pivot weak derivative is un′(t)=(2πn/T)cos⁡(2πnt/T) J(iv). Its Lq(V∗) norm is (2πn/T)∥J(iv)∥V∗(T2π∫02π∣cos⁡s∣q ds)1/q for finite q, and (2πn/T)∥J(iv)∥V∗ for q=∞. Since ⟨J(iv),v⟩=∥iv∥H2>0 by [F1], these norms grow linearly in n. Hence no positive exponent derivative bound is present.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.