Can the inverse of $ ln(x)e^x $ be finitely expressed in terms of the Lambert-W function or any other well-known transcendental functions? It is clear that a closed-form elementary function expression is unreachable.

The reason I ask is in pondering on the links between the inverse Lambert-W and some naturally arising functions of similar forms. Recall that the Lambert-W, a transcendental function, is defined as $ W(xe^x) = x. $

It is natural then to consider the inverse of functions such as $ g(x) = xe^{e^x} $ and those with further exponentiation. With a simple transformation $ z= e^x $ we can reduce $ g(x) $ to the form $ ln(z)e^z $ as originally posed. So the broader question arises: are there tangible algebraic links between the inverses of the set $$ {xe^x, xe^{e^x},xe^{e^{e^x}}}... $$

**GSO (Gliozzi-Scherk-Olive) projection** is an ingredient used in constructing a consistent model in superstring theory. The projection is a selection of a subset of possible vertex operators in the worldsheet conformal field theory (CFT)—usually those with specific worldsheet fermion number and periodicity conditions. Such a projection is necessary to obtain a consistent worldsheet CFT.

For terminology, for a compact 1-manifold as a $S^1$ circle, there are two spin structures, let one be periodic or antiperiodic in going around the circle. In string theory, these are called

Ramond (periodic)

Neveu-Schwarz (antiperiodic)

of spin structures.

For the projection to be consistent, the set $A$ of operators retained by the projection must satisfy:

Closure — The operator product expansion (OPE) of any two operators in $A$ contains only operators which are in $A$.

Mutual locality — There are no branch cuts in the OPE of any two operators in the set $A$.

Modular invariance — The partition function on the two-torus of the theory containing only the operators in $A$ respects modular invariance.

My naive questions are that

(1) whether there is a **mathematical branch** highly relevant for formulating **GSO (Gliozzi-Scherk-Olive) projection** and determine the *consistency of projection*?

My guess is that the "Modular invariance," "Closure" and "Mutual locality" may have something to do with the **symplectic geometry and Lagrangian submanifolds (of certain space)**. But I am not sure what is the precise mathematics to put these ideas together?

(2) These above are spin structure determined by Ramond (periodic) and Neveu-Schwarz (antiperiodic), say $H^1(M, \mathbb{Z}_2)$, where $M$ is the spacetime manifold. I wonder, do we have higher dimensional analogous $H^d(M, \mathbb{Z}_2)$, for higher integer $d$? If so, what is the analogous GSO projection for $H^d(M, \mathbb{Z}_2)$?

I have a electric vehicle to run a specific route which takes roughly 2hrs to complete for 24/7.

There's 3 factors I need to consider(5hrs of driving(before charging), charging at station(4hrs), chance of breakdown(10%)).

How many vehicles do I need to run 24/7 & what term do u describe this kind of study?

Thanks in Advance!

I am trying to optimise the calculation of the probability distribution poisson-inverse-gaussian

its calculation involves a half-integers modified Bessel function of the second kind. Here's a formula for the probabilistic expression.

For high input positive integer values, the calculation is very slow, as it involves a summation, or a recursion avoiding the Bessel in another formulation.

Is there an approximation for

$$K_{x-1/2}(\alpha); x >> 0$$

Thanks a lot.

Let $F_0$ and $F_1$ be compact flat manifolds of dimensions $k$ and $m$, respectively, where $k \geq m$. Suppose $f : \pi_1(F_0) \to \pi_1(F_1)$ is a surjective homomorphism. Consider the covering maps $\mathbb{R}^k \overset{\phi_0}{\longrightarrow} \mathbb{T}^k \overset{\phi_1}{\longrightarrow} F_0$ and $\mathbb{R}^m \overset{\psi_0}{\longrightarrow} \mathbb{T}^m \overset{\psi_1}{\longrightarrow} F_1$. Without loss of generality, suppose that $\phi_0$ and $\psi_0$ are the quotient maps by the standard integer lattices $\mathbb{Z}^k$ and $\mathbb{Z}^m$. Denote by $\{ e_1,\ldots,e_k \}$ and $\{ e^1,\ldots,e^m \}$ the standard bases for $\mathbb{R}^k$ and $\mathbb{R}^m$, respectively, and by $\{ [s_1],\ldots,[s_k] \}$ and $\{ [s^1],\ldots,[s^m] \}$ the standard generators for $\pi_1(\mathbb{T}^k)$ and $\pi_1(\mathbb{T}^m)$.

There exist integers $c_{ij}$ such that $f([s_i]) = \sum_j c_{ij} [s^j]$. Let $T : \mathbb{R}^k \to \mathbb{R}^m$ be the linear map defined by $T(e_i) = \sum_j c_{ij} e^j$. It's clear that $T$ descends to a map $\tilde{T} : \mathbb{T}^k \to \mathbb{T}^m$ such that the diagram $\require{AMScd}$ \begin{CD} \mathbb{R}^k @>T>> \mathbb{R}^m\\ @V \phi_0 V V @VV \psi_0 V\\ \mathbb{T}^k @>>\tilde{T}> \mathbb{T}^m \end{CD} commutes. My question is whether there exists a map $\hat{T} : F_0 \to F_1$ such that the diagram \begin{CD} \mathbb{R}^k @>T>> \mathbb{R}^m\\ @V \phi_0 V V @VV \psi_0 V\\ \mathbb{T}^k @>>\tilde{T}> \mathbb{T}^m\\ @V \phi_1 V V @VV \psi_1 V\\ F_0 @>>\hat{T}> F_1 \end{CD} commutes.

What I know: Bieberbach's second theorem states that, if $G$ and $H$ are Bieberbach subgroups of the isometry group $\mathscr{I}(\mathbb{R}^k)$, then for any isomorphism $X : G \to H$ there exists an affine bijection $S : \mathbb{R}^k \to \mathbb{R}^k$ such that $X(\beta) = S \circ \beta \circ S^{-1}$ for all $\beta \in G$. It's not difficult to show that $k = m$ if and only if $f$ is an isomorphism. In this case, it follows that $S = T$ and, therefore, $T$ descends to the desired map $\hat{T}$.

So, more specifically, my question is whether there is a generalization of Bieberbach's second theorem that implies $T$ descends when $m < k$.

Let $G$ be a split connective reductive group over $k=\mathbb F_q$, then the affine Grassmannian $X=Gr_G$ is representable by an ind-projective strict ind-scheme over $k$. (That is, there exists an inductive system of projective schemes over $\mathbb F_q$, and the maps are closed inclusions.)

Is it possible to define zeta function for $Gr_G$? And what about the analog Weil conjecture for $Gr_G$ with relations to the cohomology of $Gr_G$?

The naive example: $Gr_{GL_n}=\text{colim}_{i} \ Gr^{(i)}_{GL_n}$, one computes $\# Gr^{(i)}_{GL_n}(\Bbb F_q)= \sum_{d=0}^{\infty} a_{d,i} q^d$ is a polynomial of $q$. The limit of $\frac{a_{d,i}}{2i+1} (i \rightarrow +\infty)$ exists, and we call the limit $a_d$ and form the formal series $\sum_{d=0}^{\infty}a_dq^d \in \Bbb Z[[q]]$ . Then one define the zeta function as an element in $\Bbb Q[[q,t]]$ by the usual definition using exponential.

I have a question about estimates of hitting probabilities.

Let $B=(\{B_t\}_{t \ge 0},\{P_x\}_{x \in \mathbb{R}^d})$ be the $d$-dimensional Brownian motion starting from $x$. We assume $B$ is transient. Namely, $d \ge 3$.

Let $K$ be a compact subset of $\mathbb{R}^d$ and let $\sigma_K$ be the first hitting time of $K$: $$\sigma_{K}=\inf \{t \ge 0 \mid B_t \in K\}$$ with convention $\inf \emptyset=\infty$.

We can find the following estimate of $\sigma_K$:

\begin{align*} \frac{\Gamma(d/2)-1}{2 \pi ^{d/2}}\int_{K-x}\frac{1}{|y|^{d-2}}\,dy&=E_{x}\left[\int_{0}^{\infty}{\bf1}_{K}(X_t)\,dt \right] \\ &\ge E_{x}\left[\int_{\sigma_{K}}^{\infty}{\bf1}_{K}(X_t)\,dt :\sigma_K<\infty \right] \\ &\ge P_{x}(\sigma_K<\infty) \times \inf_{x \in K}E_{x}\left[\int_{0}^{\infty}{\bf1}_{K}(X_t)\,dt \right]. \end{align*} If $K$ has a positive measure, $E_{x}\left[\int_{0}^{\infty}{\bf1}_{K}(X_t)\,dt \right]$ is a positive function and bounded away from $0$ on compact subsets. Thus, it holds that $$P_{x}(\sigma_K <\infty) \le C \int_{K-x}|y|^{-d+2}\,dy$$ for some positive constant $C>0$ and $\lim_{|x| \to \infty}P_{x}(\sigma_K<\infty)=0$.

**My question**

Let $(E,\mu)$ be a metric measure space (locally compact). We denote $E_{\partial}=E\cup\{\partial\}$ by the one-point compactification of $E$. Let $X=(\{X_t\}_{t \ge 0},\{P_x\}_{x \in E})$ be a $\mu$-symmetric diffusion process on $(E,\mu)$. Let $K$ be a closed ball in $E$. As in the case of Brownian motion $B$, we set $$\sigma_{K}=\inf \{t \ge 0 \mid X_t \in K\}.$$ We assume $X$ is transient. Under what conditions on $X$, can we prove the next assertion: \begin{align*} (1)\quad \lim_{x \to \partial }P_{x}(\sigma_K<\infty)=0? \end{align*} Can we prove (1) without detailed heat kernel estimates?

This is the setting.

$M$ is a compact, connected Riemannian manifold without boundary. and it is isometrically embedded in some larger metric space $X$ ($X$ is not necessarily manifold). So, one can just say $M\subseteq X$.

Then, if every polyhedron $P$ such that $M\subseteq P \subseteq X$ can be retracted to $M$ in $X$, can we say $X$ itself is homotopy equivalent to $M$?

This question is motivated by the Proposition 3.2 of the paper "On neighborhoods of the Kuratowski imbedding beyond the first extremum of the diameter functinoal" by Mikhail Katz. Here is the link. https://eudml.org/doc/211844

I tried some searching. It seems that theory of ANR (absolute neighborhood retract) is related, but I'm not sure. Is this already well-known fact? If so, what is good reference for this?

Let $M$ be a $n\times n$ tridiagonal matrix, that entries are $0$ and $1$ , and such that diagonal entries are $1$. A row or a column will be said to be small, if its numer of $1$ is at most $(n+1)/2$. A row will be said 2-irreducible if it is not the conjonction of exactly two other rows. (The row $(a_1,a_2...,a_n)$ is the conjonction of the rows $(b_1,...,b_n) $ and $(c_1,...,c_n)$ iff $a_i=b_i.c_i$ for all non zero positive integer $i\leq n$).

Let's now suppose that every column is small in our matrix $M$

is there a row of $M$ that is small and 2-irreducible?

Note that if we ask $M$ to be the adjacency matrix of a lattice, then the question is equivalent to the Frankl conjecture. Note also that if one can broke the new conjecture, there is still an intermediary question by asking $M$ to be the adjacency matrix of a (finite) partial order. In a lattice $2$-irreducible and irreducible is the same notion, but in a general partial order, not being the upper bound of two distinct members is different from not being the upper bound of some subset. Indeed if we ask the same thing for "irreducible" but not 2- irreducible, one can easily build a counterexample with $M$ adjacency matrix of some partial order

I like the name "tridigonal conjecture", and I hope this name is not already tooken for another problem, but if it gets broken quickly I still have other weaker versions to propose, that are still stronger than Frankl conjecture, and the one I mentionned for partial order, such that the name "tridiagonal conjecture " can still be relevant and related to this question... (but I will mention them later if this question gets an anwer)

What is special about $\mathbb{Z}_p$-extensions which are motivic to ensure that their $\mu$ invariant is zero? Is there a simple conceptual reason.

Here are some examples.

- Let $F$ be a totally real field and $F^{cyc}$ the cyclotomic $\mathbb{Z}_p$ extension. The $\mu$ invariant of the $p$-Class group tower is conjectured to be zero. This is known when $F$ is a abelian.
- There is an analogue for quadratic imaginary fields, let $K$ be a quadratic imaginary field in which a prime $p$ splits into $\mathfrak{p}\mathfrak{p}^*$. Let $K_{\mathfrak{p}}^{\infty}/K$ be unique $\mathbb{Z}_p$-extension which is unramified outside $\mathfrak{p}$ and $K_{\mathfrak{p}^*}^{\infty}/K$ be unique $\mathbb{Z}_p$-extension which is unramified outside $\mathfrak{p}^*$. The $\mu$ invariants of these $\mathbb{Z}_p$ extensions are known to be zero (except for $p=2,3$). On the other hand, there are infinitely many other $\mathbb{Z}_p$-extensions. These $\mu$ invariants in general are not expected to vanish. These two special $\mathbb{Z}_p$-extensions come from division points on elliptic curves with complex multiplication.

There are many non-abelian analogues. Can one simply expect that a version of $\mu=0$ should hold whenever there is a motive involved?

I have the following quantity that I would like to control:

Let $Z_i$ be i.i.d. random variables with $\mathbb{E}[Z_i] = 0$ and bounded variance, for all $N\geq N_0$ large and $t\in (1/N, t_0)$ where $t_0$ is sufficiently small, I would like to get the tail estimate $$\mathbb{P} \left\{\inf_{1\leq k \leq tN} \sup_{tN \leq l \leq N} \left( \frac{1}{l-k}\sum_{i=k+1}^l Z_i \right)\leq t \right\} \leq C t^\alpha$$ for some positive $C, \alpha$. The same estimate can be rewritten as $$\mathbb{P} \left\{\inf_{1\leq k \leq tN} \sup_{tN \leq l \leq N} \left(\sum_{i=k+1}^l Z_i \right) - t(l-k) \leq 0 \right\} \leq C t^\alpha.\quad (\star)$$

To simplify the question, we can look at $$\mathbb{P} \left\{\sup_{1 \leq l \leq N} \left( \frac{1}{l}\sum_{i=1}^l Z_i \right)\leq t \right\} \leq C t^\alpha.$$ (I know the distributions of $Z_i$'s, if this is helpful).

Is there a name for this type of inequality where we look at the maximum of the averages (or the sum of i.i.d. random variables but we can not move the constant to the other side, like in $\star$ above).

I found a related general results in this paper by Chung; here the mean zero random variables are only assumed to be independent. With his notation, $S_n^* = \max_{1\leq k\leq n} |S_n|$, and $s_n = \text{Var}[S_n]$ which is $Cn$ in the i.i.d. case, we have

**Theorem 2.** If $g_n \downarrow 0$ and
$$g_n^{-1} = O((\log_2 s_n)^{1/2})$$
then we have
$$\mathbb{P}(S_n^* < g_ns_n) = (1+o(1)) \exp\left(-\frac{\pi^2}{8g_n^2}.\right)$$

Is there a simpler inequality of this type for i.i.d. random variables? The proof of this inequality in his general setting is quite technical.

**Background:**
The original event that I was trying to estimate is
$$\left\{\inf_{1\leq k \leq tN} \sup_{tN
\leq l \leq N}\sum_{i=k+1}^l X_i - Y_i \leq 0\right\}$$
where $X_i \sim \exp(\rho)$, and $Y_i \sim \exp(\rho- t)$ all independent of each other.

Like Kolmogorov or Doob's maximal inequality, maybe it is helpful to center the random variables; by defining $Z_i = X_i - Y_i - \mathbb{E}[X_i - Y_i] $, we get the centered version $$\left\{\inf_{1\leq k \leq tN} \sup_{tN \leq l \leq N}\sum_{i=k+1}^l \left(Z_i - \frac{t}{\rho(\rho-t)} \right) \leq 0 \right\},$$ and this boils down to estimate the event in my question above.

**Final remark:**
One way to get some kind of tail estimate is to go to Brownian motion using Donsker's theorem, and we could obtain
$$\limsup_{N\rightarrow \infty} \mathbb{P} \left\{\inf_{1\leq k \leq tN} \sup_{tN
\leq l \leq N} \left( \frac{1}{l-k}\sum_{i=k+1}^l Z_i \right)\leq t
\right\} \leq C t^\alpha$$ for all $t\in (0, t_0)$. In this case, the $N_0$ would be dependent on $t$ so instead of $``N\geq N_0"$ we have to use $``\limsup_N"$, and I am trying to avoid this.

**Definition:**

A linear map $f:\mathbb C^n\to \mathbb C^n$ is called **positive** if $\langle fa,a\rangle\ge0$ for all $a\in \mathbb C^n$. Equivalently, $f\in M_{n}(\mathbb C)$ is positive if it can be written in the form $g^*g$ for some $g\in M_{n}(\mathbb C)$. The unique positive element $g$ satisfying $g^2=f$ is denoted $\sqrt f$, and is called the square root of $f$.

**Definition:**

A linear map $\phi:M_{n}(\mathbb C)\to M_{m}(\mathbb C)$ is called **completely positive** if it sends positive elements to positive elements, and the same holds for $\phi\otimes id_{M_{k}(\mathbb C)}:M_{n\cdot k}(\mathbb C)\to M_{m\cdot k}(\mathbb C)$ for every $k\in\mathbb N$.

Let $e_{ij}\in M_{n}(\mathbb C)$ be the elementary matrix with a $1$ at $(i,j)$ and all other entries zero. Using the basis elementary matrices $\{e_{ij}\}$ to identify $M_{n}(\mathbb C)$ with $\mathbb C^{n^2}$, we can talk about a linear map $f:M_{n}(\mathbb C)\to M_{n}(\mathbb C)$ being positive (this has nothing to do with sending positive elements to positive elements).

**Question:**

Let $\phi:M_{n}(\mathbb C)\to M_{n}(\mathbb C)$ be a map which is both positive and completely positive. Is its square root $\sqrt\phi:M_{n}(\mathbb C)\to M_{n}(\mathbb C)$ completely positive?

**Remark:**

Maps which are both positive and completely positive are frequent. Indeed, for every completely positive map $\phi:M_{n}(\mathbb C)\to M_{m}(\mathbb C)$, its adjoint $\phi^{*}:M_{m}(\mathbb C)\to M_{n}(\mathbb C)$ is also completely positive. So $\phi^{*}\phi:M_{n}(\mathbb C)\to M_{n}(\mathbb C)$ is both positive and completely positive.

I am trying to find a function $f: \mathbb{R}^+ \to \mathbb{R}^+$ that fullfils the following conditions

$$f \in \mathcal{C}^1(\mathbb{R}^+,\mathbb{R}^+)$$

$$\int_{\mathbb{R}^+} f \in \mathbb{R}^+$$

$$\int_{\mathbb{R}^+} \mid f' \mid \in \mathbb{R}$$

$$f \text{is not $\frac{1}{2}$-Hölder}$$

I've tried functions with smooth spikes but I am unable to express this function as combinations of usual functions.

Moreover, It's worth noticing that if we have the assumption : $f'^2$ is integrable then $f$ is necessarily $\frac{1}{2}-$Hölder :

We have (using CS) : $$ \mid f(x) -f(y) \mid \leq \int_x^y 1 \times f' \leq \sqrt{\int_x^y f'^2}\sqrt{y-x} $$ Hence it follows that $f$ is $\frac{1}{2}-$Hölder continous since that $\sqrt{\int_x^y f'^2}$ is bounded.

Question: Is there an infinite sequence of primes $\{q_i\}_{i=1}^{\infty}$ that is not too sparse ( $q_n =O(poly(n))$ for a fixed polynomial) for which it is true that for every $k$ there is an $N(k)$ so that if $n>N$ then there is a prime $p$ in the interval $[q^{1/k}-o(q^{1/k}),q^{1/k})$ that is a quadratic residue modulo $q$? (by $o(q^{1/k})$ I mean does there exist an function that belongs to the class $o(q^{1/k})$ for which such a statement holds?) (Does the question become easier if we ask for a non-residue?)

Motivation: I need dense, regular, $C_{2k}$-free non bipartite graphs that are good expanders. There are constructions of dense, regular, $C_{2k}$-free graphs that are good expanders by Margulis and independently by Lubotzky, Phillips and Sarnak. These constructions depend on two primes, $p$ and $q$ and they give a suitable graph if $p$ is a quaratic residue modulo $q$, and an almost suitable but bipartite graph when $p$ is a quadratic non-residue.

Additional information: If we do not need $p$ to be a quadratic residue, bounds between consecutive primes does the job.

Edit: I realized that i accidentally posed a harder than necessary problem. For my purposes it is enough to have one such sequence for every $k$, and even the polynomial $poly(n)$ can depend on $k$.

When dealing with time-dependent PDEs, one often obtain that some quantity $E(t,x)$ belongs to a Lebesgue space $L^p_t(L^q_y)$, which means that $$\int_0^{+\infty}\|E(t,\cdot)\|_{L^q(\mathbb{R}^n)}^p dt<+\infty.$$ Sometimes, we even have $E\in L^{p_1}_t(L^{q_1}_y)\cap L^{p_2}_t(L^{q_2}_y)$ ; when this occurs, a simple interpolation, which involves only Hölder inequality, yields $E\in L^p_t(L^q_y)$ where $(\frac1p,\frac1q)$ is any point in the segment between $(\frac1{p_1},\frac1{q_1})$ and $(\frac1{p_2},\frac1{q_2})$.

I am interested in a slightly different situation, where $E\in L^{p_1}_t(L^{q_1}_y)\cap L^{q_2}_y(L^{p_2}_t)$ (the order of integrations differ in both spaces). What are the interpolation spaces ?

For instance, suppose that $E\in L^\infty_t(L^1_y)\cap L^\infty_y(L^1_t)$. What can be said of $E$ ?

Consider an array $A$ of length $n$ with $A_i \in \{1,\dots,s\}$ for some $s\geq 1$. For example take $s = 6$, $n = 5$ and $A = (2, 5, 6, 3, 1)$. Let us define $g(A)$ as the collection of sums of all the non-empty contiguously indexed subarrays of A. In this case $$g(A) = [2,5,6,3,1,7,11,9,4,13,14,10,16,15,17]$$

In this case all the sums are distinct. However, if we looked at $g((1,2,3,4))$ then the value $3$ occurs twice as a sum and so the sums are not all distinct.

For $s \geq 1$, I would like to understand what the largest $n$ is such that that there exists an array $A$ of length $n$ with all distinct $g(A)$. This question arose orginally as a coding competition and the answers for $s = 1,\dots, 21$ are $n = 1, 2, 3, 3, 4, 5, 6, 6, 7, 8, 8, 9, 10, 11, 11, 11, 12, 13, 13, 14, 14$.

On the assumption that an exact formula is hard to come by, is it possible to show its asymptotics? For example, is it true that $n$ is $\Theta(s)$?

The space $( \ell^2 ,\lVert \cdot \rVert _2 )$ is a Hilbert space. The space $X=(\ell^2 \oplus \ell^2 , \lVert \cdot \rVert_\infty )$ is a Banach space. Does X have fixed point property? (For any closed convex bounded subset $C\subseteq X $ and any nonexpansive map $T:C\to C $ there is a $x\in C$ such that $T(x)=x$)

The space $X$ isn't uniformly convex so I can't use theorems about uniformly convex. There is no theorems about F.P.P in products of spaces and I have no another idea. Does someone have any idea?

I'm studying an example in book *Yuji Shimizu and Kenji Ueno. Advances in Moduli Theory. Translations of Mathematical Monographs, vol. 206*, that shows the importance of isomorphism as principally polarized abelian varieties in Torelli's theorem.

I'm studying the following example:

For a compact Riemann surface $R$ of genus $2$, $W^1=\varphi(R)$ is isomorphic to $R$, where $\varphi:R \longrightarrow J(R)$ is the Abel map. Hence, in this case the theta divisor $\Theta$ is also a compact Riemann surface of genus $2$. Hence the Jacobian variety $J(R)$ contains a compact Riemann surface $C:=\Theta- [k]$ of genus 2, and $(J(R), [C])$ gives a principal polarization. Let $E$ be a elliptic curve. Suppose that the self product $E \times E$ contains a compact Riemann surface of genus 2 and that $E \times E$ is isomorphic to a two-dimensional abelian variety $A$. In this case $(J(C), [C])\cong (A, [C])\cong (E\times E, [C])$; isomorphisms as principally abelian varieties. On the other hand, for points $a, b \in E$ a divisor $D = a \times E+E \times b$ is ample and $(E \times E, [D])$ is also a principally polarized abelian variety. But $(E\times E, [C])$ and $(E\times E, [D])$ are not isomorphic as principally polarized abelian varieties.

A first question is: For $(E \times E, [D])$ to be a principally polarized abelian variety, it should not be that $h^0(D)=1$? If so, how do I conclude that $h^0(D)=1$?

And another question is: Why $(E\times E, [C])$ and $(E\times E, [D])$ are not isomorphic as principally polarized abelian varieties? How was this seen so quickly?

Given Hopf $\mathbb{C}$-algebra $H$, it's Hopf dual $H^o$ is the largest Hopf algebra contained in $H^*$, the $\mathbb{C}$-linear dual of $H$. (This is well known to be well-defined, see for example Sweedler book.)

If $j:G \to H$ is a linear map, then we have dual linear map $$ j^*:H^* \to G^*, ~~~~~~~~~ f \mapsto f \circ j. $$ If we restrict $j^*$ to $H^o$, then does $j^*(H^o)$ be contained in $G^o$? If $j$ is algebra map, then it is easy to show that $$ \Delta(j^*(f)) = j^*(f_{(1)}) \otimes j^*(f_{(2)}) \in G^o \otimes G^o, $$ where we use Sweedler notation. However, it $j$ is not algebra map, then it is not clear what happens. My guess is that the dual is only "functorial" for algebra maps, but it is not clear for me.

So i recently learnt that there is now a certain software called ''Coq'' by which one can check the validity of mathematical proofs. My questions are:

Are there limitations on the kinds of proofs that Coq can verify?

How long on average does Coq take to verify a proof?

Do math journals use Coq?

How do I go about it if I want to verify a proof using Coq?