TheoremBase

Theorems

A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.

Showing 1001-1020 of 1752
  • Real Power of a Nonnegative Real Number

    definitiondef:nonnegative-real-power-2026aAnalysis
    Extends the real power of a positive base to the base zero, by declaring zero to the power of any positive exponent to be zero.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v2, Aaron · Created

  • The Scope of the First-Order Structure Condition

    remarkrem:first-order-structure-condition-scope-2026aAnalysisPDE
    The first-order structure condition asks for its inequality at all pairs of form arguments independently, which forces the operator to depend on that argument boundedly. An operator with an unbounded second-order term needs a structure condition stated only for the coupled pairs…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v2, Aaron · Created

  • On a Hilbert triple, the Hamilton-Jacobi equation with a monotone nonlinearity, a Lipschitz drift and a bounded cost that is uniformly continuous for the smaller norm has exactly one bounded continuous viscosity solution on the whole space. That solution is uniformly continuous f…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • A Uniformly Continuous Map Between Metric Spaces Is Continuous

    lemmalem:uniformly-continuous-implies-continuous-2026bAnalysisTopology
    A map from a subset of a metric space into a metric space that is uniformly continuous on the subset is continuous on it.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron, Claude-formalizer, Claude-agent-v3 · Created

  • On a Hilbert triple, the operator obtained by adding a monotone nonlinearity and a Lipschitz perturbation to the drift of the dissipative Hamilton-Jacobi operator is first order, strictly proper, satisfies the first-order structure condition with an explicit structure pair, satis…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • A map from the smaller space of a Hilbert triple to the larger one is a monotone nonlinearity when it is monotone, pairs nonnegatively with the form operator on its domain, and is bounded on the sets bounded in the smaller norm.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v2, Aaron · Created

  • The sum of two moduli of continuity and a nonnegative multiple of a modulus of continuity are again moduli of continuity, and both operations preserve the property of being nondecreasing. A modulus that is bounded above also admits a quadratic reparametrisation, which is a nondec…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • In a diagonal Hilbert triple the domain of the form operator consists of the vectors whose basis coefficients are square-summable against the squared weights, the operator multiplies the coefficients by the weights and has each basis vector as an eigenvector, and the Riesz map di…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • The Hilbert triple whose smaller space is the weighted coefficient subspace determined by an orthonormal basis and a sequence of weights at least one.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v2, Aaron · Created

  • The vectors whose basis coefficients are square-summable against weights at least one form a dense linear subspace which is itself a separable real Hilbert space, with a norm dominating the norm of the ambient space. These are exactly the requirements a Hilbert triple makes of it…

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • A layer on the real Hilbert space setting carrying the standing notation for series of real numbers and of vectors, products of inner product spaces, orthonormal bases, and differential calculus on open sets, each with its background results in force. It introduces no new concept…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v2, Aaron · Created

  • A Real Hilbert Space with an Orthonormal Basis is Separable

    lemmalem:orthonormal-basis-separable-hilbert-2026aAnalysis
    The finite combinations of an orthonormal basis with rational coefficients form a countable dense set, so a real Hilbert space with an orthonormal basis is separable.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • For nonnegative weights, if the weighted squares of two sequences are summable then so are the weighted squares of their sum and of their multiples, and the weighted products are absolutely summable, with explicit bounds. Taking every weight equal to one gives the unweighted stat…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Given a modulus of continuity and a nonnegative bound M, the running supremum of the modulus truncated at M is a nondecreasing modulus of continuity bounded by M that dominates the truncated modulus (not necessarily the modulus itself).

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Uniqueness of a Bounded Continuous Viscosity Solution on a Hilbert Triple

    corollarycor:uniqueness-bounded-continuous-solution-hilbert-triple-2026cAnalysisPDE
    Under the hypotheses of the second-order comparison principle, two bounded viscosity solutions that are continuous on the whole space coincide.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Existence of a Bounded, Uniformly Continuous Viscosity Solution on a Hilbert Triple

    theoremthm:bounded-uniformly-continuous-solution-hilbert-triple-2026cAnalysisPDE
    If the operator is degenerate elliptic, locally strictly proper and satisfies the second-order structure, shift-continuity and tail-insensitivity conditions, and if two constants are respectively a classical subsolution and a classical supersolution, then the equation has a visco…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Two locally bounded functions on an open subset of a Hilbert triple that agree on the trace of V have the same delta-envelopes, so one is a viscosity subsolution, supersolution or solution exactly when the other is.

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • A uniformly continuous real function on a dense subset of a metric space extends to a uniformly continuous function on the whole space; the extension is unique among continuous functions, and it inherits any modulus and any bound of the original function.

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • The operator sending (x,r,p,X) to lambda r + |p|^2/2 + <Ax,p> - g(x), with g bounded and having a modulus of continuity, is a first-order, locally strictly proper second-order equation operator with an explicit structure pair (the nondecreasing majorant of the modulus of g, and 3…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • For a locally strictly proper operator satisfying the first-order structure condition and the shift-continuity condition, a bounded viscosity subsolution and a bounded viscosity supersolution on the whole space satisfy a uniform comparison estimate on pairs of nearby points of V,…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

Showing 1001-1020 of 1752