TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Deterministic minimax lower bound on power source balls

Statement

Assume Countable Choice. Let $K : X \to Y$ be compact between real or complex Hilbert spaces over the same scalar field, $ν, ρ > 0$ , and let $X_{ν, ρ} (K)$ be its power source ball. For any deterministic reconstruction map $A : Y \to X$ and any $δ \geq 0$ , define $E_{δ} (A) : = \sup {∥ A (K x + η) - x ∥_{X} : x \in X_{ν, ρ} (K), η \in Y, ∥ η ∥_{Y} \leq δ}$ . Then $E_{δ} (A) \geq ε_{K} (X_{ν, ρ} (K), δ)$ , and therefore $\inf_{A : Y \to X} E_{δ} (A) \geq ε_{K} (X_{ν, ρ} (K), δ)$ . For any $M \subseteq X$ with $0 \in M$ , define the two-truth modulus ${\tilde{ε}}_{K} (M, δ) : = \sup {∥ x_{1} - x_{2} ∥_{X} : x_{1}, x_{2} \in M, ∥ K (x_{1} - x_{2}) ∥_{Y} \leq 2 δ}$ . Then ${\tilde{ε}}_{K} (X_{ν, ρ} (K), δ) = 2 ε_{K} (X_{ν, ρ} (K), δ)$ .

Statement references

Compact Hilbert-space inverse model

Clason, Regularization of Inverse Problems, Theorem 4.10

Hofmann and Mathé, A Note on the Modulus of Continuity, equations (6)–(7)

Facts & Assumptions

Given: Countable Choice, compact $K : X \to Y$ between real or complex Hilbert spaces over the same scalar field, $ν, ρ > 0$ , the power source ball $X_{ν, ρ} (K)$ , a noise level $δ \geq 0$ , and a deterministic map $A : Y \to X$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is required by the compact spectral multiplier used to define the power source ball; the indistinguishable-data argument below uses no further choice.

[F1]

Power source ball: $X_{ν, ρ} (K) = {∣ K ∣^{ν} w : ∥ w ∥_{X} \leq ρ}$ .

[F2]

Centered conditional modulus of continuity: $ε_{K} (M, δ) = \sup {∥ x ∥_{X} : x \in M, ∥ K x ∥_{Y} \leq δ}$ when $0 \in M \subseteq N (K)^{⊥}$ .

[F3]

Index source elements are minimum-norm solutions: Every element of $X_{ν, ρ} (K)$ lies in $N (K)^{⊥}$ .

[F4]

Hilbert space and The induced length is a norm: The Hilbert norm is induced by the inner product, and its triangle inequality holds.

Proof

1.1givenA1F1F2F3F4choosealgebra

The class $X_{ν, ρ} (K)$ contains $0$ by taking $w = 0$ in [F1]. It is symmetric: if $x = ∣ K ∣^{ν} w$ with $∥ w ∥_{X} \leq ρ$ , then $- x = ∣ K ∣^{ν} (- w)$ with $∥ - w ∥_{X} \leq ρ$ . It is convex: for $x_{i} = ∣ K ∣^{ν} w_{i}$ with $∥ w_{i} ∥_{X} \leq ρ$ and $0 \leq t \leq 1$ , $t x_{1} + (1 - t) x_{2} = ∣ K ∣^{ν} (t w_{1} + (1 - t) w_{2})$ , while the triangle inequality gives $∥ t w_{1} + (1 - t) w_{2} ∥_{X} \leq t ρ + (1 - t) ρ = ρ$ . By [F3], this class is contained in $N (K)^{⊥}$ , so [F2] applies.

2.1givenstep 1.1F2F4algebra

Let $x \in X_{ν, ρ} (K)$ satisfy $∥ K x ∥_{Y} \leq δ$ . The two admissible truths $x$ and $- x$ with noises $- K x$ and $K x$ both produce the same observed datum $0$ . Their reconstruction errors are $∥ A (0) - x ∥_{X}$ and $∥ A (0) + x ∥_{X}$ , and the triangle inequality yields $2 ∥ x ∥_{X} = ∥ (A (0) + x) - (A (0) - x) ∥_{X} \leq ∥ A (0) + x ∥_{X} + ∥ A (0) - x ∥_{X}$ . Hence the larger error is at least $∥ x ∥_{X}$ , so taking the supremum over all such $x$ gives $E_{δ} (A) \geq ε_{K} (X_{ν, ρ} (K), δ)$ . Taking the infimum over $A$ preserves this lower bound.

3.1givenstep 1.1F1F2algebra∎

If $x_{1}, x_{2} \in X_{ν, ρ} (K)$ and $∥ K (x_{1} - x_{2}) ∥_{Y} \leq 2 δ$ , then $z = (x_{1} - x_{2}) / 2$ lies in the class by symmetry and convexity from step 1.1 and satisfies $∥ K z ∥_{Y} \leq δ$ ; thus $∥ x_{1} - x_{2} ∥_{X} = 2 ∥ z ∥_{X} \leq 2 ε_{K} (X_{ν, ρ} (K), δ)$ . Conversely, for every $z$ in the centered-modulus set, the pair $(z, - z)$ lies in the source ball and has $∥ K (z - (- z)) ∥_{Y} = 2 ∥ K z ∥_{Y} \leq 2 δ$ , so the two-truth supremum is at least $2 ε_{K} (X_{ν, ρ} (K), δ)$ . Taking suprema proves the claimed factor of two.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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.

Sources

Christian Clason, Regularization of Inverse Problems, lecture notes — Theorem 4.10 (standard reference, not scraped)
Bernd Hofmann and Peter Mathé, A Note on the Modulus of Continuity for Ill-Posed Problems in Hilbert Space (standard reference, not scraped)