/sci/ - Science & Math

>>9017830
>did you read any interesting problems, theorems, proofs, textbooks, or papers recently?
https://arxiv.org/abs/1609.02080
>Proof mining in [math] L^p [/math] spaces
>Let [math] \rho \in T^X [/math] be an admissible type. Let [math] B_{\forall}(x,u) [/math] be a [math] {\forall}-formula [/math] with at most [math] x [/math], [math] u [/math] free and [math] C_{\exists}(x,v) [/math] an [math] {\exists}-formula [/math] with at most [math] x [/math], [math] v [/math] free. Let [math] \Delta [/math] be a set of [math] {\Delta}-sentences [/math].
>Suppose that:
>[math] \mathcal{A}^{\omega} [X, \| \cdot \|, \mathcal{C}, L^p] + \Delta \vdash \forall x^{\rho} (\forall u^0 B_{\forall}(x,u) \rightarrow \exists v^0 C_{\exists}(x,v)) [/math]
>Then one can extract a partial functional [math] \Phi : S_{\hat{\rho}} \longrightarrow \mathbb{N} [/math] whose restriction to the strongly majorisable functional of [math] S_{\hat{\rho}} [/math] is a bar-recursively computable functional of [math] \mathcal{M}^{\omega} [/math] such that for all [math] L^p (\mu) [/math] Banach spaces [math] (X, \| \cdot \|) [/math] having the property that any associated set-theoretic model of it satisfies [math] \Delta [/math], we have that for all [math] \rho \in S_{\rho} [/math] and [math] x^* \in S_{\hat{\rho}} [/math] such that [math] x^* {\gtrsim}_{\rho} x [/math], the following holds:
>[math] \forall u \leq \Phi (x^*)B_{\forall}(x,u) \rightarrow \exists v \leq \Phi (x^*)C_{\exists}(x,v) [/math].
In the span of a few years we have went from conceptualising space mining on asteroids to mining proofs in abstract spaces.
Robots are underrated.