Question originally posted here, but I'm more likely to get an answer on MO. I'm looking for a reference on the following topic, should one exist. (Or a firm "stop looking and do it yourself".)

Let $H(s)=(1−s)H(0)+sH(1)$ where $s\in[0,1]$ and $H(0)$,$H(1)$ are Hermitian. Let $\lambda_0(s) < \lambda_1(s)$ be the two lowest eigenvalues of $H(s)$ and let $\gamma(s) = \lambda_1(s) - \lambda_0(s)$.

Define $I_G=\{s\in[0,1]:γ(s)≤G\}$. I'm looking for bounds of the form $\int d \mu(I_G) \leq f(G,H(0),H(1))$. Has this question previously been studied and, if so, does anyone have a reference?

Suppose $\lambda_1,\lambda_2,\cdots,\lambda_n$ are algebraic numbers. $P_1(t),P_2(t),\cdots,P_n(t)$ are polynomials with algebraic coefficients.

The question is to whether the following question is decidable. $$\sum_{i}^n P_i(t)\exp(\lambda_i t)$$ has a root $t_0>0$.

**The question.**

Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?

**Examples.**

In the current stable version of the Lean Theorem Prover, topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and today we got modular forms. There is a sort of an indication of where we are.

What else should we be doing? What should we work on next?

**Some background.**

The Lean theorem prover is a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language. You can read my personal thoughts on why I believe this sort of thing is timely and important for the pure mathematics community. Other formal proof verification software exists (Coq, Isabelle, Mizar...). I am very ignorant when it comes to other theorem provers and feel like I would like to see a comparison of where they all are.

Over the last year I have become increasingly interested in Lean's mathematics library, because it contains a bunch of what I as a number theorist regard as "normal mathematics". No issues with constructivism, the axiom of choice, quotients by equivalence relations, the law of the excluded middle or anything. My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. These paragraphs are an attempt to give an update to the community.

Let's start by getting one thing straight -- formalising deep mathematical proofs is *extremely hard*. For example, it would cost tens of millions of dollars *at least*, i.e. many many person-years, to formalize and *maintain* (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.

But formalising deep mathematical *objects* is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki in our spare time and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.

But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Whether it happens in Lean or one of the other systems -- time will tell. Tom Hales' formal abstracts project plans to formalise the statements of new theorems (in Lean) as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is *built on rigorous definitions*. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in a theorem prover and send it to Tom Hales! If you need hints about how to do that in Lean, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.

We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.

If $\Omega$ is a real analytic domain in $\mathbb R^n$, is the signed distance function, $f$, defined by \begin{equation} f(x)=\begin{cases}d(x,\partial \Omega )&{\mbox{ if }}x\in \Omega \\-d(x,\partial \Omega )&{\mbox{ if }}x\in \Omega ^{c}\end{cases} \end{equation} is real analytic? where \begin{equation} d(x,\partial \Omega ):=\inf _{y\in \partial \Omega }d(x,y)\end{equation} where inf denotes the infimum.

Thanks in advance!

I would like to know whether the reduced suspension of a Hurewicz cofibration of pointed spaces (it is a Hurewicz cofibration when considered as a map of unbased spaces) is an acyclic Hurewicz cofibration.

I think that this is wrong, but I have no counterexample so far (it will probably involve a degenerately based space).

NB: By space I mean compactly generated weak Hausdorff ones, but all perspectives could be interesting.

Let $A\in\mathbb{R}^{n\times n}$ be a nonderogatory matrix with real and strictly negative eigenvalues. Furthermore, for simplicity, suppose that $\mathrm{tr}(A)=-1$.

**Q.** I'm wondering whether it is possible to write any $A$ as above in the following particular decomposition:
$$\tag{#}\label{eq:decomp}
A=T\left(\left[\begin{array}{c|c}D_1 & 0 \\\hline 0 & 0\end{array}\right] + S\left[\begin{array}{c|c}-I_r & 0 \\\hline 0 & D_2\end{array}\right] \right)T^\top
$$
where $T\in\mathbb{R}^{n\times n}$ is an orthogonal matrix ($T^\top T=I_n$), $S\in\mathbb{R}^{n\times n}$ is a skew-symmetric matrix ($S^\top=-S$), $D_1\in\mathbb{R}^{r\times r}$ $D_2\in\mathbb{R}^{(n-r)\times (n-r)}$, $1\le r\le n$, are diagonal matrices with strictly negative entries. Note that $r$ is a further integer parameter that can vary between $1$ and $n$.

For $n=2$, I think I've managed to prove that it is always possible to write $A$ as in \eqref{eq:decomp} (see remark below). However, for $n\ge 3$ proving this fact (or finding a counterexample) seems quite hard. Thus, I would be very grateful to hear some feedback from the MO community. Thank you.

**A special case.** If $A+A^\top$ is negative definite (i.e., $A+A^\top<0$) then by decomposing $A$ as
$$
A=\underbrace{\frac{1}{2}(A+A^\top)}_{=:A_s} + \underbrace{\frac{1}{2}(A-A^\top)}_{=:A_{as}},
$$
we can select $r=n$, $T$ and $D_1$ to be the eigenvector and eigenvalue (resp.) matrix of $A_s$ (i.e., $A_s =TD_1T^\top$), and $S=-T^\top A_{as}T$. This choice yields a decomposition as in \eqref{eq:decomp}.

**$2\times 2$ case.** Let $n=2$, and (wlog) suppose that $A$ is in its Schur (upper) triangular form:
$$
A=\begin{bmatrix}a & c \\ 0 & b \end{bmatrix},
$$
where $a,b<0$, $a+b=-1$, $c\in\mathbb{R}$. Consider
$$
A_s=\frac{1}{2}(A+A^\top)=\begin{bmatrix} a & \frac{c}{2} \\ \frac{c}{2} & b \end{bmatrix},
$$

If $ab-c^2/4>0$, then $A_s<0$ and we are done (in view of the above remark). Otherwise, by virtue of the Schur-Horn Theorem, there exists an orthogonal matrix $T\in\mathbb{R}^{2\times 2}$ such that $$ T^\top A_sT = \begin{bmatrix}-1 & \sqrt{\frac{c^2}{4}-ab} \\ \sqrt{\frac{c^2}{4}-ab} & 0 \end{bmatrix}. $$ Next, consider $$ A_{as}=\frac{1}{2}(A-A^\top)=\begin{bmatrix} 0 & \frac{c}{2} \\ -\frac{c}{2} & 0 \end{bmatrix} $$ and notice that, under the previous orthogonal $T$, $A_{as}$ is still skew-symmetric and so it remains unchanged (up to a $\pm 1$). Thus, we have \begin{align} A=A_s+A_{as}&=T\left(\begin{bmatrix}-1 & \sqrt{\frac{c^2}{4}-ab} \\ \sqrt{\frac{c^2}{4}-ab} & 0 \end{bmatrix} + \begin{bmatrix} 0 & \frac{c}{2} \\ -\frac{c}{2} & 0 \end{bmatrix}\right)T^\top\\ &=T\left(\begin{bmatrix}-1 & 0 \\ 0 & 0 \end{bmatrix} + \begin{bmatrix} 0 & \sqrt{\frac{c^2}{4}-ab}+\frac{c}{2} \\ \sqrt{\frac{c^2}{4}-ab}-\frac{c}{2} & 0 \end{bmatrix}\right)T^\top. \end{align} Finally, by picking $r=1$, $$S=\begin{bmatrix} 0 & \sqrt{\frac{c^2}{4}-ab}-\frac{c}{2} \\ -\sqrt{\frac{c^2}{4}-ab}+\frac{c}{2} & 0 \end{bmatrix},\quad D_2= \frac{\sqrt{\frac{c^2}{4}-ab}+\frac{c}{2}}{\sqrt{\frac{c^2}{4}-ab}-\frac{c}{2}}<0, $$ we obtain a decomposition as in \eqref{eq:decomp}.

Suppose we are considering $S_n$. For any permutation, let $h$ be the number of derangement and $N$ be the number of cycles no less than 2.

I'm interested in the number of permutations such that $h-N=k$. I do not need an exact value. An upper bound depending on $n$ and $k$ for large $n$ is enough. I also have a guess of the order of the upper bound: $$(n/\sqrt{2k})^{2k}$$ I come up with this guess due to the fact that if $h-N=k$, $h$ must be smaller or equal to $2k$. In the case $h=2k$, we have $$\frac{n(n-1)\cdots(n-2k+1)}{(2k)!!}$$ permutations which is roughly the above order. I also guess this case should dominate other cases when $k+1\leq h<2k$, which results in my conjecture.

Denote by $S_r$ the usual circle of radius $r$, with the path metric ($d(x,y) = r\theta$, where $\theta$ is the angle between the vectors $x$ and $y$), and let $\alpha \in (1/2,1)$. Consider the collection of mappings $f: S_r \rightarrow \mathbb{R}^2$ satisfying $|f(x) - f(y)| \leq d(x,y)^\alpha$ for all $x,y \in \mathbb{R}^2$ (no other assumptions on $f$). It makes sense to talk about the area enclosed by $f(S_r)$, basically by taking the integral over $\mathbb{R}^2$ of the winding number relative to $f(S_r)$. Notice that the constraints on $\alpha$ imply that $f(S_r)$ has zero area.

The question then is: what mapping $f$ maximizes this enclosed area? Thinking about the problem for a few minutes would suggest that this would be a circle, as in the classical isoperimetric problem, though with a different radius (which, it seems, is usually impossible to write down explicitly).

The problem seems difficult. The difficulty is that it's inherently global: starting from a given $f$, one can usually expand at a point $x$ without violating the Hölder condition locally, though this might violate the Hölder condition for $x$ relative to a point far away.

I'm curious if it this question has been asked before and whether it would be a tractable problem.

If $X\subset \mathbb{P}^n$ is a smooth hypersurface (more generally a complete intersection) of dimension at least 2, and if $K_X+\mathscr{O}_X(-1)\geq 0$, why is it true that $H^0(T_X(1))=0$?

(Source: *On a conjecture of Clemens on rational curves on hypersurfaces*, paragraph before Proposition 1.1)

Given a large enough prime $p$ are there four coprimes $A,B,C,D$ of roughly equal size of either $p^{2/5}$ or $p^{3/8}$ such that the smallest $|M|,|N|,|M'|,|N'|$ (taken in range $(-p/2,p/2)$) with $$ADN-BCM\equiv ACM'-BDN'\equiv0\bmod p$$ $$(M+N)(AC+BD)\equiv(M'+N')(AD+BC)\bmod p$$ holding true can be roughly $p^{2/5}$ or $p^{3/8}$ for each of the cases respectively?

Note $$Det\Bigg(\begin{bmatrix} -BC&AD&0&0\\ 0&0&-BD&AC\\ AC+BD&AC+BD&0&0\\ 0&0&AD+BC&AD+BC\end{bmatrix}\Bigg)=-(A D + B C)^2 (A C + B D)^2\not\equiv0\bmod p$$ and so there is lot of flexibility (http://www.wolframalpha.com/input/?i=Det%7B%7B-BC,AD,0,0%7D,%7B0,0,-BD,AC%7D,%7BAC%2BBD,AC%2BBD,0,0%7D,%7B0,0,AD%2BBC,AD%2BBC%7D%7D%2F%2FFullSimplify).

My computations indicate nothing better than $p^{3/4}$ in both scenarios.

Let $X$ be a toric variety containing the $n$-torus $T\overset{i}{\hookrightarrow} X$. The action of $T$ extends naturally to an action on the sheaf $i_*\mathcal{O}_T$ by

$$(\alpha\cdot f)(x):=f(\alpha^{-1}x) \; \; \forall \, f\in (i_*\mathcal{O}_T)(U),\forall \alpha\in T$$ on each invariant open set $U\subseteq X$.

Now, given a coherent $\mathcal{O}_X$-module $\mathcal{F}\leq i_*\mathcal{O}_T$ we say that it is equivariant if we can restrict the above action of $T$ to $\mathcal{F}$.

I whant to know if the following is true

Two equivariant sheaves $\mathcal{F_1}$ and $\mathcal{F_2}$ are isomorphic as $\mathcal{O}_X$-modules if and only if they are isomorphic as $T$-equivariant $\mathcal{O}_X$-modules, i.e, there is an isomorphism commuting with the action of $T$.

This appear to be a consequence of Theorem 9.II in Chapter 1 of the book Toroidal Embeddings I of Mumford et al. but it can as well be just a typo (there is no proof for that part).

I would like to differentiate this matrix A with respect to a vector x: $$A = x^tBxy^tx$$

where B is a known matrix. y is a vector with the same dimension with x. I tried to google but only found the result for quadratic form, not cubic like this

Let $M$ be a simply connected space form (i.e. $\mathbb R^n$, sphere, or hyperbolic space) and $B$ be a ball in $M$. Let $\phi$ be the first Laplacian eigenfunction on $B$, with respect to the Dirichlet boundary condition $\phi=0$ on $\partial B$.

In Cheng's remarkable paper "Eigenvalue comparison theorems and its geometric applications", it is remarked that (p. 290) "since all simply connected space forms are two-point homogeneous, $\phi$ is a radial function". I think two-point homogeneity means that there always exists an isometry mapping one pair of points to any other pair of points which have the same distance apart (is it?). I don't understand how this condition is used.

I think the reason why $\phi$ is radial is that we can apply the spherical mean of it to obtain $\widetilde \phi$, which is also an eigenfunction as rotation preserves the metric. If $\widetilde \phi\ne \phi$, then $h=\phi-\widetilde \phi$ is a first eigenfunction that changes sign, which is a contradiction. But I don't see where the "two-point homogeneous condition" is used. (Is there an alternate proof?)

If my argument is correct it should also apply to balls centered at 0 of the warped product space $dr^2+f(r)^2 d\theta^2$. Is this well-known? If so, is there a quick reference?

Let $X$ be a Banach space, $T(t)$ be a strongly continuous semigroup on $X$, and $f\in L^1(0,\tau;X)$. It has been implied that the integral $$v(t)=\int_0^t T(t-s)f(s)ds,\quad t\in [0,\tau]$$ is not always an element of $W^{1,1}(0,\tau;X)$. That seems odd to me. Can anyone think of an example?

Recall the integer partition function $P(n)$ with generating function $$\sum_{n\geq0}P(n)x^n=\prod_{k=1}^{\infty}\frac1{1-x^k}.$$ Let $[n]_q=\frac{1-q^n}{1-q}$ denote the $q$-analogue of the integer $n$ and let $\lambda=(\lambda_1,\lambda_2,\dots)\vdash n$ be a partition of $n$. Now, define the function $$\Psi_q(n)=\sum_{\lambda\vdash n}\,\,\sum_{j\geq1}\,\, [\lambda_j]_q.$$ For example, $\Psi_q(3)=[3]_q+([2]_q+[1]_q)+([1]_q+[1]_q+[1]_q)=q^2+2q+6$. In particular, when $q=1$, we obtain $\Psi_q(n)=nP(n)$ with generating function $$\sum_{n\geq1}nP(n)x^n=x\frac{d}{dx}\prod_{k=1}^{\infty}\frac1{1-x^k}.$$

I would like to ask

**Question 1.** Is there a generating function for the sequence of $q$-polynomials $\Psi_q(n)$?

**Question 2.** What is the combinatorial interpretation of the coefficients of $\Psi_q(n)$?

For example, the constant term of $\Psi_q(n)$ enumerates the number of $1$'s in all partitions of $n$.

Let $A\in \mathbb R^{n\times n},\ b\in \mathbb R^n$ such that $\forall x\in \{-1,1\}^n : Ax\ne b$.

Let us denote: $S=\{x\in\mathbb R^n|Ax=b\}$ ('S' for solution set).

Is $\ \#\Big\{H\in\big\{ \{-1\}, \{1\}, (-1,1)\big\}^n \ \Big|\ H\cap S\ne\emptyset\ \Big\} = O(n)$?

where '#' denotes the cardinality of the set.

My intuition tells me that this should be true, but I can't figure out how to prove or disprove it.

So far, I've done many trial and error "experiments" that also support my conjecture, but I am stuck in proving/ disproving it in the general case.

I am interested in some cohomological algebras related to toric manifolds. We consider a toric manifold $M$ as a quotient $$M = P^{-1}(p) / \mathbb{K}, \quad P : \mathbb{C}^n \to \text{Lie}(\mathbb{K})^*,$$ where $P$ is the momentum map associated with the linear action of a torus $\mathbb{K} \subset (S^1)^n$ on $\mathbb{C}^n$, and $p$ is a regular value of $P$.

The cohomology of $M$ can be expressed in terms of two ideals in the algebra $\mathbb{C}[u_1,...,u_n]$ of polynomial functions on $\mathbb{C}^n := \text{Lie}((S^1)^n) \otimes \mathbb{C}$, the exponents $m = (m_1,...,m_n)$ of which we view as elements of $\ker(\exp : \text{Lie}(\mathbb{R}^{n}) \to (S^1)^n)$:

- $I$ the ideal of polynomials vanishing on $\mathbb{C}^k := \text{Lie}(\mathbb{K}) \otimes \mathbb{C} \subset \mathbb{C}^n$;
- $J$ the ideal generated by monomials $u^m := u_1^{m_1}...u_n^{m_n}$ such that $m$, considered as a function on $\mathbb{R}^{n*} = \text{Lie}((S^1)^n)^*$, assumes strictly positive values on the polyhedron $(i^*)^{-1}(p) \cap \mathbb{R}^{n*}_{>0}$, where $i^* : \mathbb{R}^{n*} \to \text{Lie}(\mathbb{K})^*$ is the map induced by the inclusion $\mathbb{K} \overset{i}{\hookrightarrow} (S^1)^n$.

We have: $$H^*(M,\mathbb{C}) \simeq \mathbb{C}[u_1,...,u_n]\ / \ (I+J).$$

Let me modify $J$ a little bit, and define the following submodule $J_r$ of $\mathbb{C}[u_1,...,u_n]$: $$J_r \text{ is generated by monomials } u^m \text{ for which } \ m \in \ker(\exp : \text{Lie}(\mathbb{K}) \to \mathbb{K}) \ \text{ and } \ p(m) \geq r.$$

Notice that for $r > 0$, we have $J_r \subset J$.

It is well-known that the cohomology of any smooth projective variety (in particular $M$) is a finite dimensional vector space over $\mathbb{C}$. However, I have trouble understanding why the same property should be true for the cohomological algebra

$$\mathbb{C}[u_1,...,u_n] \ / \ (I + J_r).$$

I would be grateful if someone had an idea.

Suppose we have a circle of radius $r$ centered at the origin $(0,0)$. The number of integer lattice points within the circle, $N$, can be bounded using Gauss circle problem .

Suppose that another circle of radius $r/2$ centered at the origin inside the initial circle of radius $r$, let $N^*$ represents the number of integer lattice points within the the smallest circle. I am mainly interested in the relation between $N$ and $N^*$. More precisely, to find the number of integer lattice points within the circle of radius $r$ and outside(and at the boundary of) the circle of radius $r/2$.

This page provides the number $N$ for some distances $r$ in $2$ dimensions. For example if we take "ignore the integer lattice point represents the origin":

$r=4$, then $N^*=12, N=48 $ and $N^* = \frac{1}{4}N$

$r=6$, then $N^*=28, N=112 $ and $N^* = \frac{1}{4}N$

.

.

.

$r=40$, then $N^*=1256, N=5024 $ and $N^* = \frac{1}{4}N$

By doing more calculations, in general (considering $r$ is even *for simplicity) we can say $$\frac{1}{5}N \leq N^* \leq \frac{1}{3}N$$

I searched in the literature to find something about this relation in $2$ or $d$ dimensions but without success. I think there is a result or a bound about it, could you kindly direct me to a reference or to a bound and I would be very grateful.

In the book "Representation of Semisimple Lie Algebra in the BGG Category $\mathcal{O}$".

**Exercise 1.13.** Suppose $\lambda\not\in\Lambda$, so the linkage class $W\cdot\lambda$ is the disjoint union of its nonempty intersections with various cosets of $\Lambda_r$ in $\mathbb{h}^*$. Prove that each $M\in\mathcal{O}_{\chi_\lambda}$ has a corresponding direct sum decomposition $M=\oplus_i M_i$, in which all weights of $M_i$ lies in a single coset.

*My attempt:*

$M=\bigoplus_{\nu\in\mathfrak{h}^*} M_\nu =\bigoplus_{[\nu]\in\mathfrak{h}^*/\Lambda_r} M^{[\nu]}$.

Since $\mathfrak{g}_\alpha\cdot M_\mu\subseteq M_{\mu+\alpha}$ for all $\alpha\in \Phi$, we get $U(\mathfrak{n})\cdot M^{[\nu]}\subseteq M^{[\nu]}$, $U(\mathfrak{h})\cdot M^{[\nu]}\subseteq M^{[\nu]}$ and $U(\mathfrak{n}^-)\cdot M^{[\nu]}\subseteq M^{[\nu]}$.

Since $U(\mathfrak{g})=U(\mathfrak{n}^-)U(\mathfrak{h})U(\mathfrak{n})$, we get $U(\mathfrak{g})\cdot M^{[\nu]}\subseteq M^{[\nu]}$. Hence $M^{[\nu]}$ is a $U(\mathfrak{g})$-submodule of $M$.

Since $M\in\mathcal{O}$, $M$ is finitely generated as a $U(\mathfrak{g})$-module. Therefore, $M=\bigoplus_{i=1}^n M^{[\nu_i]}$.

Now, let $W\cdot\lambda=\{\eta_1,\cdots,\eta_k\}$. Consider $\{\eta_{i_1},\cdots, \eta_{i_r}\}\subseteq \{\eta_1,\cdots,\eta_k\}$ such that $[\eta_{i_1}],\cdots, [\eta_{i_r}]$ are distinct and $\{[\eta_{i_1}],\cdots, [\eta_{i_r}]\}=\{[\eta_1],\cdots,[\eta_k]\}$. It is clearly that $W\cdot\lambda\cap[\eta]\neq \emptyset\implies [\eta]\in \{ [\eta_{i_1}],\cdots, [\eta_{i_r}]\}$.

Then $W\cdot \lambda =\bigcup_{\eta\in\mathfrak{h}^*} W\cdot\lambda \cap[\eta] =\bigsqcup_{j=1}^{r}W\cdot\lambda \cap[\eta_{i_j}] =\bigsqcup_{j=1}^{r}W\cdot \eta_{i_j} \cap[\eta_{i_j}] =\bigsqcup_{j=1}^{r}W_{[\eta_{i_j}]}\cdot \eta_{i_j}$

I would like to know whether the ** corresponding direct sum decomposition** means $M=\bigoplus_{j=1}^r M^{[\eta_{i_j}]}$.
If so, how to prove it? Also, am I on the right track?

I have the following linear matrix inequality:

$$F^T P + PF < 0,$$

where $P$ is a positive definite matrix and $F$ is a matrix with appropriate dimension.

Let $Q$ be a positive definite matrix that obeys $Q \leq P$. Is this equivalence valid?

$$F^TP+PF< 0 \iff F^TQ+QF< 0$$