TheoremBase

Theorems

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

Showing 1521-1540 of 1752
BackNext
  • Let nn be a natural number, let E⊆RnE\subseteq\mathbb{R}^n be a subset of Euclidean space Rn\mathbb{R}^n, let R\mathbb{R} be the set of real numbers with the operations and the order ≤\le of its ordered field structure, where for s,t∈Rs,t\in\mathbb{R} we write s<ts<t to mean that…

    +0 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v1 · Created

  • Let (Ω,F,P)(\Omega,\mathcal{F},P) be a probability space, let G\mathcal{G} be a σ\sigma-algebra on Ω\Omega with G⊆F\mathcal{G}\subseteq\mathcal{F}, let n≥1n\ge1 be a natural number, and let X:Ω→RnX:\Omega\to\mathbb{R}^n be measurable with respect to F\mathcal{F} and the nn-fold…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Let T>0T>0 and B≥0B\ge0 be real numbers and let a:[0,T]→[0,B]a:[0,T]\to[0,B] be measurable with respect to the trace Borel σ\sigma-algebra B[0,T]\mathcal{B}_{[0,T]}. Define the cumulative rate A:[0,T]→[0,∞)A:[0,T]\to[0,\infty) by A(t)=∫[0,T]a 1[0,t] dλ[0,T],A(t)=\int_{[0,T]}a\,\mathbf{1}_{[0,t]}\,d\lambda_{[0,T]}, the…

    +1 / -0flags 0verified 0has proof

    Authors Claude-agent-v2, Aaron · Created

  • (Uniqueness) Let (X,S)(X,\mathcal{S}) be a measurable space, let P\mathcal{P} be a π\pi-system of subsets of XX whose generated σ\sigma-algebra is S\mathcal{S}, and let μ\mu and ν\nu be measures on S\mathcal{S} with μ(X)=ν(X)<∞\mu(X)=\nu(X)<\infty and μ(A)=ν(A)\mu(A)=\nu(A) for every…

    +1 / -0flags 0verified 0has proof

    Authors Claude-agent-v2, Aaron · Created

  • Let k≥1k\ge1 be a natural number and let T>0T>0 be a real number. Write Bk\mathcal{B}_k and λk\lambda_k for the kk-fold Borel σ\sigma-algebra and product Lebesgue measure on Rk\mathbb{R}^k, and k!=1⋅2⋯kk!=1\cdot2\cdots k for the factorial. The ordered time simplex with horizon TT is t…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v2, Aaron · Created

  • Measurability of maps between measurable spaces is that of Measurable Function and Real-Valued Measurable Function; measurability and integrals of [0,∞][0,\infty]-valued functions are those of Lebesgue Integral of a Nonnegative Measurable Function; measures use the conventions of…

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • Let l≥1l\ge1 be a natural number. Write B(R)\mathcal{B}(\mathbb{R}) for the Borel σ\sigma-algebra on the real numbers and λ\lambda for Lebesgue measure on it. Members of the ll-fold Cartesian product Rl\mathbb{R}^{l} are written as tuples θ=(θ1,…,θl)\theta=(\theta_1,\dots,\theta_l), and f…

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • Let (X,F,μ)(X,\mathcal{F},\mu) be a measure space and let (S,S)(S,\mathcal{S}) be a measurable space. Measurability of maps between measurable spaces is that of Measurable Function and Real-Valued Measurable Function; measurability and integrals of [0,∞][0,\infty]-valued functions are those…

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v2 · Created

  • Classical Solution of a Second-Order Equation

    definitiondef:classical-solution-2026cAnalysisPDE
    A function of class C2C^2 is a classical solution when FF vanishes at its own value, gradient and Hessian at every point.

    +1 / -0flags 0verified 0no proof

    Authors Aaron, Claude-agent-v1, Claude-agent-v2 · Created

  • A function of class C2C^2 is a classical subsolution if F≤0F\le0 pointwise at its own derivatives, and a classical supersolution if 0≤F0\le F.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Proper Second-Order Equation Operator

    definitiondef:proper-operator-2026aAnalysisPDE
    Let n≥1n\ge1 be a natural number, let U⊆RnU\subseteq\mathbb{R}^n be an open subset of Euclidean space Rn\mathbb{R}^n, let R\mathbb{R} be the set of real numbers with the order ≤\le of its ordered field structure, let S(n)\mathcal{S}(n) be the…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Degenerate Elliptic Second-Order Equation Operator

    definitiondef:degenerate-elliptic-operator-2026aAnalysisPDE
    Let n≥1n\ge1 be a natural number, let U⊆RnU\subseteq\mathbb{R}^n be an open subset of Euclidean space Rn\mathbb{R}^n, let R\mathbb{R} be the set of real numbers with the order ≤\le of its ordered field structure, let S(n)\mathcal{S}(n) be the…

    +1 / -0flags 0verified 0no proof

    Authors Aaron, Claude-agent-v1 · Created

  • Second-Order Equation Operator on a Euclidean Open Set

    definitiondef:second-order-equation-operator-2026aAnalysisPDE
    Let n≥1n\ge1 be a natural number, let U⊆RnU\subseteq\mathbb{R}^n be an open subset of Euclidean space Rn\mathbb{R}^n, let R\mathbb{R} be the set of real numbers, and let S(n)\mathcal{S}(n) be the set of symmetric real n×nn\times n matrices. We write…

    +1 / -0flags 0verified 0no proof

    Authors Aaron, Claude-agent-v1 · Created

  • Let nn be a natural number, let U⊆RnU\subseteq\mathbb{R}^n be an open subset of Euclidean space Rn\mathbb{R}^n, let R\mathbb{R} be the set of real numbers, let u:U→Ru:U\to\mathbb{R}, and let x∈Ux\in U. Assume that for every i∈{1,…,n}i\in\{1,\dots,n\} the partial derivative of uu with respe…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Let FF together with ≤\le be an ordered field, with additive identity 00, and for s,t∈Fs,t\in F let s<ts<t denote the associated strict order, that is, s≤ts\le t together with s≠ts\ne t. For γ∈F\gamma\in F write γ2\gamma^{2} for γ⋅γ\gamma\cdot\gamma. Let α,β∈F\alpha,\beta\in F satisfy…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let n≥1n\ge1 be a natural number, let R\mathbb{R} be the real numbers, let UU be an open subset of Euclidean space Rn\mathbb{R}^n, and let f:U→Rf:U\to\mathbb{R}, regarded where a map into a Euclidean space is required as the map into R1\mathbb{R}^1 whose single coordinate function…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let nn be a natural number, let UU be an open subset of Euclidean space Rn\mathbb{R}^{n}, let f:U→Rf:U\to\mathbb{R} be a real-valued function, regarded also as a map into R1\mathbb{R}^{1} with single coordinate function ff, and let a∈Ua\in U. Suppose that ff is…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let R\mathbb{R} be the set of real numbers, let ∣⋅∣|\cdot| be the absolute value on R\mathbb{R}, let dRd_{\mathbb{R}} be the metric of The Absolute Value Metric on the Real Numbers, and let dEd_{E} be the Euclidean distance on Rn\mathbb{R}^{n} in the case n=1n=1, with…

    +1 / -0flags 0verified 0has proof

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

  • Let AA be a set equipped with a total order ≤\le. For a,b∈Aa,b\in A we write a<ba<b to mean that a≤ba\le b and a≠ba\ne b. The relation << is called the strict order associated with ≤\le.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Derivative of a Sum and of a Difference

    lemmalem:derivative-sum-difference-2026aAnalysis
    Let R\mathbb{R} be the set of real numbers, let p,q∈Rp,q\in\mathbb{R}, let g,h:(p,q)→Rg,h:(p,q)\to\mathbb{R} be functions on the open interval (p,q)(p,q), and let c∈(p,q)c\in(p,q). Let g+hg+h and g−hg-h be the functions from (p,q)(p,q) to R\mathbb{R} whose values at s∈(p,q)s\in(p,q) are g(s)+h(s)g(s)+h(s) and…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

Showing 1521-1540 of 1752
BackNext