TITLE: Simple: Angle Between Two Angles of Circle
QUESTION [5 upvotes]: I want to be able to define a start and an end angle in a circle and then be able to come up with an algorithm that allows me to test if an angle is between the two angles (clockwise from start to end). Note that this has to work if the start point is 300deg and the end point is 45degrees. So for example,
start=10, end=50, test=20   (inside)
start=270, end=90, test=350 (inside)
start=270, end=90, test=180 (outside)
start=310, end=20, test=0 (inside)
start=310, end=20, test=200 (outside)
Thanks so much!

REPLY [11 votes]: Start by subtracting the start angle from all angles.
If any angles are now negative, add $360^\circ$ to them.
Now check to see if the middle angle is smaller than the end angle.

Example $1$: Is $180^\circ$ between $270^\circ$ and $90^\circ$?

Subtract to get start and end angles $0^\circ$, $-180^\circ$, with midpoint $-90^\circ$
Add $360^\circ$ to get $0^\circ$, $180^\circ$, with midpoint $270^\circ$
Since $270^\circ > 180^\circ$, $180^\circ$ is not between $270^\circ$ and $90^\circ$.

Example $2$: Is $0^\circ$ between $310^\circ$ and $20^\circ$?

Subtract to get start and end angles $0^\circ$, $-290^\circ$, with midpoint $-310^\circ$
Add $360^\circ$ to get $0^\circ$, $70^\circ$, with midpoint $50^\circ$
Since $50^\circ < 70^\circ$, $0^\circ$ is between $310^\circ$ and $20^\circ$.

And in C / C++:
bool isBetween(float start, float end, float mid) {
    end = (end - start) < 0.0f ? end - start + 360.0f : end - start;
    mid = (mid - start) < 0.0f ? mid - start + 360.0f : mid - start;
    return (mid < end);
}


text:
\section{PROBLEM DESCRIPTION}
The scenario described in Section \ref{scenario} is based on the k-center or k-median problem, depending on the objective function. The uncapacitated facility location problem was first described in \cite{Balinski1965}. For a given amount of $V$ locations, a predefined amount of $K$ central locations have to be found. The k-center problem considers the minimization of the maximum distance between a location and its nearest center \cite{Chaudhuri1998}. In contrast, k-median problem uses the median as objective criterion \cite{Jain2001}. Both problems are NP-hard \cite{Gonzalez85}. The problem can be specified using a strongly connected graph topology \mbox{$G(V,E)$} with vertices ($v_{ i } \in V{}\ with{}\ i :=\{1,..,n\}$) and edges ($e_{ p } \in E{}\ with{}\ p :=\{1,..,m\}$).

The k-center problem is defined on a complete, undirected graph. The objective function $d$ defines the fitness value d($v_i$,$v_j$) for an edge e($v_{i}$,$v_{j}$) between two vertices ($v_{i}$,$v_{j}$), satisfying the triangle inequality. The objective function $d$ selects the best edge from a vertex $v_{i}$ to one of the calculated locations of a center node ($k_{u} \in K{}\ with{}\ u :=\{1,..,l\}\ and{}\ l \leq n $). A center node $k_{u}$ can be a vertice, dependent on the placement constraint from Section \ref{introduction}. The amount of all fitness values $d$ from every vertice $v_{i}$ is defined as $D$.

We intend to place the amount $K$ of center nodes to minimize the maximum $d$($v_{i}$, $k_{u}$) from a vertex $v_{i}$ to its \mbox{closest $k_{u}$.} This objective criterion belongs to the typical k-center problem according to Equation \ref{form:max}, the objective criterion of the similar k-median problem correspond to Equation \ref{form:med}:

\vspace*{-0.3cm}

\begin{equation}
D_{center}(K) = \underset{ } { min }\text{ } \underset{v_i = 1, ..., n }{ max } \text{ } \underset{ k_u \in K } {min}\text{ } d(v_i, k_u)
\label{form:max}
\end{equation}

\vspace*{-0.1cm}

\begin{equation}
D_{median}(K) = \underset{  } { min }\text{ }  \sum_{ v_i = 1 }^n { } \text{ } \underset{ k_u \in K } {min}   \text{ } d(v_i, k_u)
\label{form:med}
\end{equation}

\vspace*{-0.3cm}

Regarding our case, we set up a predefined amount $K$ of warehouses and minimize the maximum distance $D$ from the stores $V$ to its nearest warehouse $k$. The objective function $d$ defines the distance between a warehouse $k_{u}$ and a store $v_i$.

config: arxiv


TITLE: inverse of a tridiagonal matrix
QUESTION [5 upvotes]: Let
$${A_{n \times n}} = \left[ {\begin{array}{*{20}{c}}
{-2}&{1}&{}&{}&{}\\
{1}&{-2}&{1}&{}&{}\\
{}&{1}&{\ddots}&{\ddots}&{}\\
{}&{}&{\ddots}&{\ddots}&{1}\\
{}&{}&{}&{1}&{-2}
\end{array}} \right]$$
be a tridiagonal matrix. How we can prove that its inverse is the matrix $B=(b_{ij})$ where
$$b_{ij}=-\frac{i(n+1-j)}{n+1} \; ,\quad i\leq j.$$

REPLY [3 votes]: As Henning points out, checking that two matrices are inverses is much easier than computing an inverse; all we need to do is find the product of the matrices.  Also, note that your definition of $B$ is incomplete, but we can deduce the rest since $B$ must be symmetric.
By definition, the $i,j$ of the matrix product $AB$ is given by
$$
[AB](i,j) = \sum_{k=1}^n a_{ik}b_{kj}
$$
in the case of $i=1$, we have
$$
[AB](1,j) = \sum_{k=1}^n a_{1k}b_{kj} = \\
\begin{cases}
-2\cdot\frac{1(n+1 - j)}{n+1}
+ 1 \cdot \frac{2(n + 1 - j)}{n+1} & j \geq 2\\
-2 \cdot \frac{1(n+1-j)}{n+1}
+ 1  \cdot \frac{j(n + 1 - 2)}{n+1} & j=1
\end{cases} = \delta_{ij}
$$
We can repeat a similar computation for the cases $2 \leq i \leq n-1$ and $i = n$.

Alternatively: we can find the characteristic polynomial of $A$ using induction (Pavel's method).  From there, we could find the inverse using the Cayley Hamilton theorem.


TITLE: How do you figure out what are all the possible numbers that four variables can be for a given N?
QUESTION [2 upvotes]: I know what I want to do but I do not know how to do it. This is complication that I have, there are four variables A, B, C, D which all are ≥ 1. So in the equation (A+B+C+D)=N where I know what N equal to; how do I find the possible values of A, B, C, D?

EDIT:
To clarify A, B, C, D are four variables with the value of ≥ 1 and the relationship that they have the sum of one number.
So, in the equation...
(A+B+C+D)=N
How do you figure out what are all the possible numbers that A, B, C, D can be for a given N?

P.S. I have just started learning mathematics with a new passion, I really enjoy it and have been relearning and learning a lot of stuff. If you could also point me in the direction of information that work with problems like these, that would be great!

REPLY [1 votes]: Here are two possible answers given two different interpretations of your question.  I'm guessing you're interested in the first answer.
Answer 1
If by variable you mean positive integers, and $N$ is also a positive integer, then you can think of a solution to the equation $A+B+C+D=N$ as a placement of $N$ balls into $4$ boxes with the requirement that each box has at least $1$ ball.  This is the same as placing $N-4$ balls into four boxes with no requirements.  The answer to the number of ways to do this is
$$\binom{N-1}{3}=\frac{(N-1)!}{3!(N-4)!}=\frac{(N-1)(N-2)(N-3)}{6}=\frac{1}{6}N^3-N^2+\frac{11}{6}N-1$$
Notice this only makes sense if $N\ge 4$.  To see this, consider a collection of symbols consisting of $N-4$ circles (representing the balls) and $3$ vertical lines (representing a separation of the balls).  Altogether, there are $N-1$ symbols.  Orderings of these symbols correspond exactly to placements of the balls into four boxes, where we treat the vertical lines as the markers for when one box stops and another begins (notice we only need $3$ of them to delineate $4$ boxes).  To order these symbols, we really only need to choose where we put the $3$ lines, which gives the result above.
This isn't an algorithm for writing down all possible solutions, but it lets you know how many you need to write down.
Answer 2
If by variables you mean real numbers, then the equation $A+B+C+D=N$ with the requirement that $A,B,C$, and $D$ all be no less than $1$ has infinitely many solutions for $N>4$, 1 solution for $N=4$, and no solutions for $N< 4$.  I won't elaborate here unless this is actually the question you were asking.

REPLY [1 votes]: To list them all, you're going to need to use some kind of algorithm.  The most obvious is three nested for loops.  For example, in GAP we have:
N:=8;;
for A in [1..N-3] do
  for B in [1..N-A-2] do
    for C in [1..N-A-B-1] do
      D:=N-A-B-C;
      Print([A,B,C,D],"\n");
    od;
  od;
od;

Above, some tweaks are made so that $A,B,C,D$ are all $\geq 1$ (if we didn't make these tweaks in the code above, $D$ might end up being $0$ or negative; this could be handled by not outputting the answer when $D \leq 0$).  I chose N:=8;; arbitrarily.
This will output:
[ 1, 1, 1, 5 ]
[ 1, 1, 2, 4 ]
[ 1, 1, 3, 3 ]
[ 1, 1, 4, 2 ]
[ 1, 1, 5, 1 ]
[ 1, 2, 1, 4 ]
[ 1, 2, 2, 3 ]
[ 1, 2, 3, 2 ]
[ 1, 2, 4, 1 ]
[ 1, 3, 1, 3 ]
[ 1, 3, 2, 2 ]
[ 1, 3, 3, 1 ]
[ 1, 4, 1, 2 ]
[ 1, 4, 2, 1 ]
[ 1, 5, 1, 1 ]
[ 2, 1, 1, 4 ]
[ 2, 1, 2, 3 ]
[ 2, 1, 3, 2 ]
[ 2, 1, 4, 1 ]
[ 2, 2, 1, 3 ]
[ 2, 2, 2, 2 ]
[ 2, 2, 3, 1 ]
[ 2, 3, 1, 2 ]
[ 2, 3, 2, 1 ]
[ 2, 4, 1, 1 ]
[ 3, 1, 1, 3 ]
[ 3, 1, 2, 2 ]
[ 3, 1, 3, 1 ]
[ 3, 2, 1, 2 ]
[ 3, 2, 2, 1 ]
[ 3, 3, 1, 1 ]
[ 4, 1, 1, 2 ]
[ 4, 1, 2, 1 ]
[ 4, 2, 1, 1 ]
[ 5, 1, 1, 1 ]

If you're after a mathematical description, the definition you give is already quite succinct; we could write it in set notation as: $$\{(A,B,C,D) \in (\mathbb{Z}_{\geq 1})^4:A+B+C+D=N\}.$$


TITLE: a problem on test of converges of two series
QUESTION [1 upvotes]: Test the following series for convergence:
(a)$$ \sum_{n=1}^\infty \frac{(n+1)^n}{n^{n+5/4}}$$
(b)$$\sum_{n=1}^\infty \frac{\tan \left(\frac{1}{n} \right)}{\sqrt{n}}.$$

Which formula/test would be useful to solve this problem?

REPLY [0 votes]: Use the Kummer's Test:

Given a series $\sum_{i=1}^{\infty}u_i$ of positive terms $u_i$ and a sequence of finite positive constants $a_i$, let
  $$
\rho=\lim_{n\to\infty}\left(a_n\cdot\frac{ u_n}{u_{n+1}}-a_{n+1}\right).
$$

If $\rho>0$, the series converges.
If $\rho<0$ and the series $\sum_{n=1}^{\infty}1/a_n$ diverges, the series diverges.
If $\rho=0$, the series may converge or diverge.

The test is a general case of Bertrand's test, the root test, Gauss's test, and Raabe's test. With $a_n=n$ and $a_{(n+1)}=n+1$, the test becomes Raabe's test.


TITLE: How to integrate $sec^{3}x$
QUESTION [0 upvotes]: How do  I integrate $sec^{3}x$. I have done this by converting $sec$ to $cos$ and then using $cos^{3}x= (1-sin^{2}x)cosx$ and then putting sinx=t and then using partial fractions. But this is very long method. I want shorter method for this
Thanks

REPLY [1 votes]: $$\int \sec^3 (x)\,dx$$

Hint:
Use the reduction formula, $\color{gray}{\displaystyle\int \sec^k(x)\,dx=\frac{\sin(x)\sec^{k-1}(x)}{k-1}+\frac{k-2}{k-1}\displaystyle\int \sec^{-2+k}(x)\,dx}$
$$=\frac 1 2 \tan(x)\sec(x)+\frac1 2 \int \sec(x)\,dx$$
Multiply numerator and denominator of $\sec(x)$ by $\tan(x)\sec(c)$:
$$=\frac 1 2 \tan(x)\sec(x)+\frac 1 2 \displaystyle\int \frac{\sec^2(x)+\sec(x)\tan(x)}{\sec(x)+\tan(x)}\,dx$$


TITLE: Proving commutativity of convolution $(f \ast g)(x) = (g \ast f)(x)$
QUESTION [20 upvotes]: From any textbook on fourier analysis:
"It is easily shown that for $f$ and $g$, both $2 \pi$-periodic functions on $[-\pi,\pi]$, we have $$(f \ast g)(x) = \int_{-\pi}^{\pi}f(x-y)g(y)\;dy = \int_{-\pi}^{\pi}f(z)g(x-z)\;dz = (g \ast f)(x),$$ by using the substitution $z = x-y.$"

I don't doubt that this is true, but I cannot figure out what happened to the negative sign coming from $dy = -dz\;$ after the change of variable $z = x - y$.  In particular, after the change of variable $z = x-y,\;$ I am coming up with $ -\int_{-\pi}^{\pi}f(z)g(x-z)\;dz$. What am I missing here?

REPLY [6 votes]: \begin{align*}
\\&\int_0^tf(t-u)g(u)\cdot\text du\\
\\\text{let } v=t-u\\
\text dv=-\text du\\
\\ u=0\rightarrow v=t\\u=t\rightarrow v=0\\
&=\int_t^0f(v)g(t-v)\cdot -\text dv\\
&=\int_0^tf(v)g(t-v)\cdot \text dv\\
\\&\\
\\&\\
\\&\\
\\&\\
\end{align*}
\begin{align*}\mathcal L\left\{\int\limits_0^tf(t-u)g(u)\cdot\text du\right\}
&=\int\limits_0^\infty\int\limits_0^t f(t-u)g(u)\cdot\text du\cdot e^{-pt}\cdot\text dt\\
&=\int\limits_0^\infty e^{-pt}\int\limits_0^t f(t-u)g(u)\cdot\text du\cdot\text dt\\
u=0\rightarrow t=u\\
u=t \rightarrow t=\infty\\
&=\int\limits_0^\infty g(u)\int\limits_u^\infty e^{-pt}f(t-u)\cdot\text dt\cdot\text du\\
\text{let }v=t-u\\
\text dv =\text dt\\
t=u\rightarrow v=0\\
t=\infty \rightarrow v=\infty\\
&=\int\limits_0^\infty g(u)\int\limits_{0}^\infty e^{-p(v+u)}f(v)\cdot\text dv\cdot\text du\\
&=\int\limits_0^\infty g(u)e^{-up}\cdot\text du\times\int\limits_{0}^\infty f(v)e^{-pv}\cdot\text dv\\
\\&=G(p)F(p)
\end{align*}


text:
import algebra.homology.homological_complex
import category_theory.abelian.exact
import for_mathlib.homological_complex_shift
import for_mathlib.split_exact
import category_theory.triangulated.rotate
import algebra.homology.homotopy_category
import algebra.homology.additive
import for_mathlib.homological_complex_abelian
import for_mathlib.homotopy_category
import for_mathlib.triangle

noncomputable theory

universes v u

open_locale classical

open category_theory category_theory.limits

namespace homological_complex

variables {V : Type u} [category.{v} V] [abelian V]
variables (A B C : cochain_complex V ℤ) (f : A ⟶ B) (g : B ⟶ C)

@[simp, reassoc]
lemma homotopy.comp_X_eq_to_iso {X Y : cochain_complex V ℤ} {f g : X ⟶ Y} (h : homotopy f g)
  (i : ℤ) {j k : ℤ} (e : j = k) : h.hom i j ≫ (Y.X_eq_to_iso e).hom = h.hom i k :=
by { subst e, simp }

@[simp, reassoc]
lemma homotopy.X_eq_to_iso_comp {X Y : cochain_complex V ℤ} {f g : X ⟶ Y} (h : homotopy f g)
  {i j : ℤ} (e : i = j) (k : ℤ) : (X.X_eq_to_iso e).hom ≫ h.hom j k = h.hom i k :=
by { subst e, simp }

@[simp]
lemma X_eq_to_iso_shift (n i j : ℤ) (h : i = j) :
  X_eq_to_iso (A⟦n⟧) h = A.X_eq_to_iso (congr_arg _ h) := rfl

@[simp, reassoc]
lemma retraction_X_eq_to_hom (h : ∀ i, splitting (f.f i) (g.f i)) {i j : ℤ} (e : i = j) :
  (h i).retraction ≫ (A.X_eq_to_iso e).hom = (B.X_eq_to_iso e).hom ≫ (h j).retraction :=
by { subst e, simp,}

@[simp, reassoc]
lemma section_X_eq_to_hom (h : ∀ i, splitting (f.f i) (g.f i)) {i j : ℤ} (e : i = j) :
  (h i).section ≫ (B.X_eq_to_iso e).hom = (C.X_eq_to_iso e).hom ≫ (h j).section :=
by { subst e, simp }

def cone.X : ℤ → V := λ i, A.X (i + 1) ⊞ B.X i

variables {A B C}

def cone.d : Π (i j : ℤ), cone.X A B i ⟶ cone.X A B j :=
λ i j, if hij : i + 1 = j then biprod.lift
  (biprod.desc (-A.d _ _)                         0        )
  (biprod.desc (f.f _ ≫ (B.X_eq_to_iso hij).hom) (B.d _ _))
else 0

/-- The mapping cone of a morphism `f : A → B` of homological complexes. -/
def cone : cochain_complex V ℤ :=
{ X := cone.X A B,
  d := cone.d f,
  shape' := λ i j hij, dif_neg hij,
  d_comp_d' := λ i j k (hij : _ = _) (hjk : _ = _),
  begin
    substs hij hjk,
    apply biprod.hom_ext; ext; simp [cone.d],
  end }

@[simp]
lemma cone_X (i : ℤ) : (cone f).X i = (A.X (i + 1) ⊞ B.X i) := rfl

@[simp]
lemma cone_d : (cone f).d = cone.d f := rfl

def cone.in : B ⟶ cone f :=
{ f := λ i, biprod.inr,
  comm' := λ i j hij,
  begin
    dsimp [cone_d, cone.d], dsimp at hij, rw [dif_pos hij],
    ext;
    simp only [comp_zero, category.assoc, category.comp_id,
      biprod.inr_desc, biprod.inr_fst, biprod.lift_fst, biprod.inr_snd, biprod.lift_snd],
  end }

local attribute [instance] endofunctor_monoidal_category discrete.add_monoidal

def cone.out : cone f ⟶ A⟦(1 : ℤ)⟧ :=
{ f := λ i, biprod.fst,
  comm' := λ i j (hij : _ = _),
  begin
    subst hij,
    dsimp [cone_d, cone.d],
    ext; simp,
  end }

@[simps]
def cone.triangle : triangulated.triangle (cochain_complex V ℤ) :=
{ obj₁ := A,
  obj₂ := B,
  obj₃ := cone f,
  mor₁ := f,
  mor₂ := cone.in f,
  mor₃ := cone.out f }

variable (V)

@[simps]
def _root_.homotopy_category.lift_triangle :
  triangulated.triangle (cochain_complex V ℤ) ⥤
    triangulated.triangle (homotopy_category V (complex_shape.up ℤ)) :=
{ obj := λ t, triangulated.triangle.mk _
    ((homotopy_category.quotient _ _).map t.mor₁)
    ((homotopy_category.quotient _ _).map t.mor₂)
    ((homotopy_category.quotient _ _).map t.mor₃),
  map := λ t t' f,
  { hom₁ := (homotopy_category.quotient _ _).map f.hom₁,
    hom₂ := (homotopy_category.quotient _ _).map f.hom₂,
    hom₃ := (homotopy_category.quotient _ _).map f.hom₃,
    comm₁' := by { dsimp, rw [← functor.map_comp, ← functor.map_comp, f.comm₁] },
    comm₂' := by { dsimp, rw [← functor.map_comp, ← functor.map_comp, f.comm₂] },
    comm₃' := by { dsimp, rw [← functor.map_comp, ← functor.map_comp, f.comm₃] } },
  map_id' := λ X, by { ext; exact category_theory.functor.map_id _ _  },
  map_comp' := λ X Y Z f g, by { ext; exact category_theory.functor.map_comp _ _ _ } }

variable {V}

@[simps]
def cone.triangleₕ : triangulated.triangle (homotopy_category V (complex_shape.up ℤ)) :=
(homotopy_category.lift_triangle _).obj (cone.triangle f)

section cone_functorial

variables {f} {A' B' : cochain_complex V ℤ} {f' : A' ⟶ B'} {i₁ : A ⟶ A'} {i₂ : B ⟶ B'}
variables (comm : homotopy (f ≫ i₂) (i₁ ≫ f'))

include comm

def cone.map : cone f ⟶ cone f' :=
{ f := λ i, biprod.lift
  (biprod.desc (i₁.f _) 0)
  (biprod.desc (comm.hom _ _) (i₂.f _)),
  comm' := λ i j r,
  begin
    change i+1 = j at r,
    dsimp [cone_d, cone.d],
    simp_rw dif_pos r,
    apply category_theory.limits.biprod.hom_ext;
      simp only [biprod.lift_desc, add_zero, preadditive.comp_neg, category.assoc,
        comp_zero, biprod.lift_fst, biprod.lift_snd]; ext,
    { simp },
    { simp },
    { simp only [X_eq_to_iso_f, preadditive.comp_add, biprod.inl_desc_assoc, category.assoc,
        preadditive.neg_comp],
      have := comm.comm (i+1),
      dsimp at this,
      rw [reassoc_of this],
      subst r,
      simpa [prev_d, d_next, ← add_assoc] using add_comm _ _ },
    { simp }
  end }

@[simp, reassoc]
lemma cone.in_map : cone.in f ≫ cone.map comm = i₂ ≫ cone.in f' :=
by ext; { dsimp [cone.map, cone.in], simp }

@[simp, reassoc]
lemma cone.map_out : cone.map comm ≫ cone.out f' = cone.out f ≫ i₁⟦(1 : ℤ)⟧' :=
by ext; { dsimp [cone.map, cone.out], simp }

omit comm

-- I suppose this is not true?
-- def cone.map_homotopy_of_homotopy' (comm' : homotopy (f ≫ i₂) (i₁ ≫ f')) :
--   homotopy (cone.map comm) (cone.map comm') := by admit

@[simps]
def cone.triangleₕ_map : cone.triangleₕ f ⟶ cone.triangleₕ f' :=
{ hom₁ := (homotopy_category.quotient _ _).map i₁,
  hom₂ := (homotopy_category.quotient _ _).map i₂,
  hom₃ := (homotopy_category.quotient _ _).map $ cone.map comm,
  comm₁' := by { dsimp [cone.triangleₕ], simp_rw ← functor.map_comp,
    exact homotopy_category.eq_of_homotopy _ _ comm },
  comm₂' := by { dsimp [cone.triangleₕ], simp_rw ← functor.map_comp, simp },
  comm₃' := by { dsimp [cone.triangleₕ], simp_rw ← functor.map_comp, simp } }

@[simps]
def cone.triangle_map (h : f ≫ i₂ = i₁ ≫ f') : cone.triangle f ⟶ cone.triangle f' :=
{ hom₁ := i₁,
  hom₂ := i₂,
  hom₃ := cone.map (homotopy.of_eq h),
  comm₁' := by simpa [cone.triangle],
  comm₂' := by { dsimp [cone.triangle], simp },
  comm₃' := by { dsimp [cone.triangle], simp } }

@[simp]
lemma cone.map_id (f : A ⟶ B) :
  cone.map (homotopy.of_eq $ (category.comp_id f).trans (category.id_comp f).symm) = 𝟙 _ :=
by { ext; dsimp [cone.map, cone, cone.X]; simp }

@[simp]
lemma cone.triangle_map_id (f : A ⟶ B) :
  cone.triangle_map ((category.comp_id f).trans (category.id_comp f).symm) = 𝟙 _ :=
by { ext; dsimp [cone.map, cone, cone.X]; simp }

def cone.triangle_functorial :
  arrow (cochain_complex V ℤ) ⥤ triangulated.triangle (cochain_complex V ℤ) :=
{ obj := λ f, cone.triangle f.hom,
  map := λ f g c, cone.triangle_map c.w.symm,
  map_id' := λ X, cone.triangle_map_id _,
  map_comp' := λ X Y Z f g, by { ext; dsimp [cone.map, cone, cone.X]; simp } }

-- I suppose this is also not true?
-- def cone.triangleₕ_functorial :
--   arrow (homotopy_category V (complex_shape.up ℤ)) ⥤
--     triangulated.triangle (homotopy_category V (complex_shape.up ℤ)) :=
-- { obj := λ f, cone.triangleₕ f.hom.out,
--   map := λ f g c, @cone.triangleₕ_map _ _ _ _ _ _ _ _ _ c.left.out c.right.out
--   begin
--     refine homotopy_category.homotopy_of_eq _ _ _,
--     simpa [-arrow.w] using c.w.symm
--   end,
--   map_id' := by admit,
--   map_comp' := by admit }

open_locale zero_object

lemma homological_complex.zero_X {ι : Type*} {c : complex_shape ι}
  {C : homological_complex V c} (hC : is_zero C) (i : ι) :
  is_zero (C.X i) :=
begin
  rw [is_zero_iff_id_eq_zero, ← homological_complex.eval_obj,
    ← (homological_complex.eval V c i).map_id, hC.eq_of_src (𝟙 C) 0],
  refl
end

def cone_from_zero (A : cochain_complex V ℤ) : cone (0 : 0 ⟶ A) ≅ A :=
{ hom :=
  { f := λ i, biprod.snd, comm' := begin
      introv r, ext; dsimp [cone.d] at *;
      simp only [if_pos r, zero_comp, dite_eq_ite, biprod.lift_snd,
        biprod.inl_desc, biprod.inr_desc, biprod.inl_snd_assoc, biprod.inr_snd_assoc],
    end },
  inv := cone.in _,
  inv_hom_id' := by { intros, ext, dsimp [cone.in], simp only [biprod.inr_snd] },
  hom_inv_id' := begin
    ext; dsimp [cone.in];
    simp only [biprod.inl_snd_assoc, zero_comp, comp_f, id_f, category.assoc,
      category.comp_id, biprod.inl_fst, biprod.inl_snd, biprod.inr_fst, biprod.inr_snd,
      biprod.inr_snd_assoc],
    apply is_zero.eq_of_src,
    apply homological_complex.zero_X,
    apply limits.is_zero_zero,
  end }

def cone_to_zero (A : cochain_complex V ℤ) : cone (0 : A ⟶ 0) ≅ A⟦(1 : ℤ)⟧ :=
{ hom := cone.out _,
  inv :=
    { f := λ i, biprod.inl, comm' := begin
        introv r, ext; dsimp [cone.d] at *;
        simp only [if_pos r, zero_comp, comp_zero, dite_eq_ite, category.assoc, category.comp_id,
          biprod.lift_fst, biprod.lift_snd, biprod.inl_desc, neg_smul, one_zsmul,
          biprod.inl_fst, biprod.inl_snd],
    end },
  hom_inv_id' := begin
    ext; dsimp [cone.out];
    simp only [biprod.inl_snd_assoc, zero_comp, comp_f, id_f, category.assoc,
      category.comp_id, biprod.inl_fst, biprod.inl_snd, biprod.inr_fst, biprod.inr_snd,
      biprod.inl_fst_assoc, biprod.inr_fst_assoc],
    apply is_zero.eq_of_src,
    apply homological_complex.zero_X,
    apply limits.is_zero_zero,
  end,
  inv_hom_id' := by { intros, ext, dsimp [cone.out], simp } }

def cone.desc_of_null_homotopic (h : homotopy (f ≫ g) 0) : cone f ⟶ C :=
cone.map (h.trans (homotopy.of_eq (comp_zero.symm : 0 = 0 ≫ 0))) ≫ (cone_from_zero _).hom

def cone.lift_of_null_homotopic (h : homotopy (f ≫ g) 0) : A ⟶ cone g⟦(-1 : ℤ)⟧ :=
(shift_shift_neg A (1 : ℤ)).inv ≫ (shift_functor _ (-1 : ℤ)).map ((cone_to_zero _).inv ≫
  cone.map (h.trans (homotopy.of_eq (comp_zero.symm : 0 = 0 ≫ 0))).symm)

@[simps]
def of_termwise_split_mono [H : ∀ i, split_mono (f.f i)] : B ⟶ B' :=
{ f := λ i, i₂.f i - (H i).retraction ≫ comm.hom i (i-1) ≫ B'.d (i-1) i -
    B.d i (i+1) ≫ (H (i+1)).retraction ≫ comm.hom (i+1) i,
  comm' := λ i j (r : i + 1 = j), by { subst r, simp only [d_comp_d, sub_zero, category.assoc,
    comp_zero, preadditive.comp_sub, hom.comm, preadditive.sub_comp, zero_comp, sub_right_inj,
    d_comp_d_assoc], congr; ring } }

@[simp, reassoc]
lemma of_termwise_split_mono_commutes [H : ∀ i, split_mono (f.f i)] :
  f ≫ of_termwise_split_mono comm = i₁ ≫ f' :=
begin
  ext i,
  dsimp,
  have : f.f i ≫ i₂.f i = A.d i (i + 1) ≫ comm.hom (i + 1) i + comm.hom i (i - 1) ≫
    B'.d (i - 1) i + i₁.f i ≫ f'.f i := by simpa [d_next, prev_d] using comm.comm i,
  simp only [hom.comm_assoc, preadditive.comp_sub, this],
  erw [split_mono.id_assoc, split_mono.id_assoc],
  simp [add_right_comm]
end

def of_termwise_split_mono_homotopy [H : ∀ i, split_mono (f.f i)] :
  homotopy i₂ (of_termwise_split_mono comm)  :=
{ hom := λ i j, (H i).retraction ≫ comm.hom i j,
  zero' := λ _ _ r, by rw [comm.zero _ _ r, comp_zero],
  comm := λ i,
    by { simp [d_next, prev_d], abel } }

@[simps]
def of_termwise_split_epi [H : ∀ i, split_epi (f'.f i)] : A ⟶ A' :=
{ f := λ i, i₁.f i + comm.hom i (i-1) ≫ (H (i-1)).section_ ≫ A'.d (i-1) i +
    A.d i (i+1) ≫ comm.hom (i+1) i ≫ (H i).section_,
  comm' := λ i j (r : i + 1 = j), by { subst r, simp only [add_zero, d_comp_d, preadditive.comp_add,
    category.assoc, comp_zero, add_right_inj, hom.comm, zero_comp, preadditive.add_comp,
    d_comp_d_assoc], congr; ring } }

@[simp, reassoc]
lemma of_termwise_split_epi_commutes [H : ∀ i, split_epi (f'.f i)] :
  of_termwise_split_epi comm ≫ f' = f ≫ i₂ :=
begin
  ext i,
  dsimp,
  have : f.f i ≫ i₂.f i = A.d i (i + 1) ≫ comm.hom (i + 1) i + comm.hom i (i - 1) ≫
    B'.d (i - 1) i + i₁.f i ≫ f'.f i := by simpa [d_next, prev_d] using comm.comm i,
  simp only [this, category.assoc, preadditive.add_comp, ← f'.comm],
  erw [split_epi.id, split_epi.id_assoc],
  rw [add_comm, add_comm (i₁.f i ≫ f'.f i), ← add_assoc, category.comp_id]
end

def of_termwise_split_epi_homotopy [H : ∀ i, split_epi (f'.f i)] :
  homotopy (of_termwise_split_epi comm) i₁ :=
{ hom := λ i j, comm.hom i j ≫ (H j).section_,
  zero' := λ _ _ r, by rw [comm.zero _ _ r, zero_comp],
  comm := λ i,
    by { simp [d_next, prev_d], abel } }

end cone_functorial

section termwise_split_mono_lift

@[simps]
def termwise_split_mono_lift (f : A ⟶ B) : A ⟶ biproduct B (cone (𝟙 A)) :=
biproduct.lift f (cone.in _)

@[simps]
def termwise_split_mono_desc (f : A ⟶ B) : biproduct B (cone (𝟙 A)) ⟶ B :=
biproduct.fst

@[simps]
def termwise_split_mono_section (f : A ⟶ B) : B ⟶ biproduct B (cone (𝟙 A)) :=
biproduct.inl

@[simp, reassoc] lemma termwise_split_mono_section_desc (f : A ⟶ B) :
  termwise_split_mono_section f ≫ termwise_split_mono_desc f = 𝟙 _ :=
by { ext, simp }

lemma termwise_split_mono_desc_section_aux (i : ℤ) :
  𝟙 (B.X i ⊞ (A.X (i + 1) ⊞ A.X i)) = biprod.snd ≫ biprod.desc (𝟙 (A.X (i + 1))) (A.d i (i + 1)) ≫
    biprod.inl ≫ biprod.inr + biprod.snd ≫ biprod.snd ≫
    (X_eq_to_iso A (sub_add_cancel i 1).symm).hom ≫ biprod.inl ≫ biprod.lift
    (biprod.desc (-A.d (i - 1 + 1) (i + 1)) 0) (biprod.desc (X_eq_to_iso A (sub_add_cancel i 1)).hom
    (A.d (i - 1) i)) ≫ biprod.inr + biprod.fst ≫ biprod.inl :=
begin
  ext1; simp only [zero_comp, preadditive.comp_add, zero_add, add_zero, biprod.inr_fst_assoc,
    biprod.inl_fst_assoc, biprod.inl_snd_assoc, biprod.inr_snd_assoc, category.comp_id],
  ext1, { simp },
  ext1, { simp only [add_zero, preadditive.add_comp, comp_zero, biprod.inr_fst, category.assoc] },
  ext1; simp,
end

def termwise_split_mono_desc_section (f : A ⟶ B) :
  homotopy (𝟙 _) (termwise_split_mono_desc f ≫ termwise_split_mono_section f) :=
{ hom := λ i j, if h : i = j + 1 then
    biprod.snd ≫ biprod.snd ≫ (A.X_eq_to_iso h).hom ≫ biprod.inl ≫ biprod.inr else 0,
  zero' := λ i j r, dif_neg (ne.symm r),
  comm := λ i, by { dsimp,
    simpa [d_next, prev_d, cone.d] using termwise_split_mono_desc_section_aux i } }

instance (f : A ⟶ B) (i : ℤ) : split_mono ((termwise_split_mono_lift f).f i) :=
{ retraction := biprod.snd ≫ biprod.snd, id' := by simp [cone.in] }

-- generalize to epi
@[simp]
lemma termwise_split_mono_lift_desc (f : A ⟶ B) :
  termwise_split_mono_lift f ≫ termwise_split_mono_desc f = f :=
by { ext, simp }

/-- We will prove this is iso later -/
def from_termwise_split_mono_lift_triangleₕ :
  cone.triangleₕ (termwise_split_mono_lift f) ⟶ cone.triangleₕ f :=
cone.triangleₕ_map
  (homotopy.of_eq ((termwise_split_mono_lift_desc f).trans (category.id_comp f).symm))

@[simps]
def termwise_split_mono_factor_homotopy_equiv : homotopy_equiv (biproduct B (cone (𝟙 A))) B :=
{ hom := termwise_split_mono_desc f,
  inv := termwise_split_mono_section f,
  homotopy_hom_inv_id := (termwise_split_mono_desc_section f).symm,
  homotopy_inv_hom_id := homotopy.of_eq (termwise_split_mono_section_desc f) }

end termwise_split_mono_lift

section termwise_split_epi_lift

@[simps]
def termwise_split_epi_lift (f : A ⟶ B) : A ⟶ biproduct A (cone (𝟙 (B⟦(-1 : ℤ)⟧))) :=
biproduct.inl

@[simps]
def termwise_split_epi_desc (f : A ⟶ B) : biproduct A (cone (𝟙 (B⟦(-1 : ℤ)⟧))) ⟶ B :=
biproduct.desc f (cone.out _ ≫ (shift_neg_shift _ _).hom)

@[simps]
def termwise_split_epi_retraction (f : A ⟶ B) : biproduct A (cone (𝟙 (B⟦(-1 : ℤ)⟧))) ⟶ A :=
biproduct.fst

@[simp, reassoc] lemma termwise_split_epi_lift_retraction (f : A ⟶ B) :
  termwise_split_epi_lift f ≫ termwise_split_epi_retraction f = 𝟙 _ :=
by { ext, simp }

lemma termwise_split_epi_retraction_lift_aux (i : ℤ) :
  𝟙 (A.X i ⊞ (B.X (i + 1 - 1) ⊞ B.X (i - 1))) = biprod.snd ≫ biprod.desc (𝟙 _)
  (-B.d (i + -1) (i + 1 + -1)) ≫ 𝟙 _ ≫ biprod.inl ≫ biprod.inr + biprod.snd ≫ biprod.snd ≫
  ((B⟦(-1 : ℤ)⟧).X_eq_to_iso (sub_add_cancel _ _).symm).hom ≫ biprod.inl ≫ biprod.lift
  (biprod.desc (B.d (i - 1 + 1 + -1) (i + 1 + -1)) 0) (biprod.desc
  ((B⟦(-1 : ℤ)⟧).X_eq_to_iso $ sub_add_cancel _ _).hom (-B.d (i - 1 + -1) (i + -1))) ≫
  biprod.inr + biprod.fst ≫ biprod.inl :=
begin
  ext1; simp only [category.comp_id, add_zero, category.id_comp, preadditive.comp_add,
    biprod.inl_snd_assoc, zero_add, zero_comp, biprod.inl_fst_assoc, biprod.inr_fst_assoc,
    biprod.inr_snd_assoc],
  ext1, { simp },
  simp only [biprod.inr_desc_assoc, preadditive.neg_comp_assoc, X_eq_to_iso_shift,
    biprod.inr_snd_assoc, preadditive.comp_add, category.assoc, preadditive.neg_comp],
  ext1, { simp only [add_zero, preadditive.add_comp, comp_zero,
    preadditive.neg_comp, biprod.inr_fst, neg_zero, category.assoc] },
  ext; simp; refl
end

def termwise_split_epi_retraction_lift (f : A ⟶ B) :
  homotopy (𝟙 _) (termwise_split_epi_retraction f ≫ termwise_split_epi_lift f) :=
{ hom := λ i j, if h : i = j + 1 then
    biprod.snd ≫ biprod.snd ≫ ((B⟦(-1 : ℤ)⟧).X_eq_to_iso h).hom ≫ biprod.inl ≫ biprod.inr else 0,
  zero' := λ i j r, dif_neg (ne.symm r),
  comm := λ i, by { dsimp,
    simpa [d_next, prev_d, cone.d] using termwise_split_epi_retraction_lift_aux i } }

instance (f : A ⟶ B) (i : ℤ) : split_epi ((termwise_split_epi_desc f).f i) :=
{ section_ := (B.X_eq_to_iso $ eq_add_neg_of_add_eq rfl).hom ≫ biprod.inl ≫ biprod.inr,
  id' := by { dsimp, simp [cone.out] } }

end termwise_split_epi_lift

section termwise_split_exact

variables (f g)

@[simps]
def connecting_hom (h : ∀ (i : ℤ), splitting (f.f i) (g.f i)) : C ⟶ A⟦(1 : ℤ)⟧ :=
{ f := λ i, (h i).section ≫ B.d i (i + 1) ≫ (h (i + 1)).retraction,
  comm' :=
  begin
    intros i j r,
    induction r,
    dsimp,
    rw ← cancel_mono (𝟙 _),
    swap, apply_instance,
    conv_lhs { rw ← (h _).ι_retraction },
    simp only [preadditive.comp_neg, one_zsmul, category.assoc, neg_smul, preadditive.neg_comp,
      ← f.comm_assoc, (h _).retraction_ι_eq_id_sub_assoc, preadditive.sub_comp_assoc,
      preadditive.sub_comp, preadditive.comp_sub, category.id_comp, d_comp_d_assoc,
      zero_comp, comp_zero, ← g.comm_assoc, (h i).section_π_assoc],
    simp,
  end }

@[simps]
def triangle_of_termwise_split (h : ∀ (i : ℤ), splitting (f.f i) (g.f i)) :
  triangulated.triangle (cochain_complex V ℤ) :=
triangulated.triangle.mk _ f g (connecting_hom f g h)

@[simps]
def triangleₕ_of_termwise_split (h : ∀ (i : ℤ), splitting (f.f i) (g.f i)) :
  triangulated.triangle (homotopy_category V (complex_shape.up ℤ)) :=
(homotopy_category.lift_triangle V).obj (triangle_of_termwise_split f g h)

@[simps]
def homotopy_connecting_hom_of_splittings (h h' : ∀ (i : ℤ), splitting (f.f i) (g.f i)) :
  homotopy (connecting_hom f g h) (connecting_hom f g h') :=
{ hom := λ i j, if e : j + 1 = i then
    ((h' i).section ≫ (h i).retraction ≫ (A.X_eq_to_iso e).inv) else 0,
  comm := λ i, begin
    rw ← cancel_epi (g.f _),
    { dsimp,
      simp [d_next, prev_d, splitting.π_section_eq_id_sub_assoc, -retraction_X_eq_to_hom],
      abel },
    exact (h i).epi
  end,
  zero' := λ _ _ h, dif_neg h }

@[simps]
def triangleₕ_map_splittings_hom (h h' : ∀ (i : ℤ), splitting (f.f i) (g.f i)) :
  triangleₕ_of_termwise_split f g h ⟶ triangleₕ_of_termwise_split f g h' :=
{ hom₁ := 𝟙 _,
  hom₂ := 𝟙 _,
  hom₃ := 𝟙 _,
  comm₃' :=
  begin
    simp only [category.comp_id, triangleₕ_of_termwise_split_mor₃, category.id_comp,
      category_theory.functor.map_id],
    apply homotopy_category.eq_of_homotopy,
    exact homotopy_connecting_hom_of_splittings f g h h'
  end }

@[simps]
def triangleₕ_map_splittings_iso (h h' : ∀ (i : ℤ), splitting (f.f i) (g.f i)) :
  triangleₕ_of_termwise_split f g h ≅ triangleₕ_of_termwise_split f g h' :=
{ hom := triangleₕ_map_splittings_hom f g h h',
  inv := triangleₕ_map_splittings_hom f g h' h,
  hom_inv_id' := by { ext; exact category.comp_id _ },
  inv_hom_id' := by { ext; exact category.comp_id _ } }

end termwise_split_exact
section

variables {B'' B' : cochain_complex V ℤ} {b' : B'' ⟶ B} {b : B ⟶ B'}
variables (H₂ : ∀ i, splitting (f.f i) (g.f i))
variables (h₂ : homotopy (b' ≫ g) 0) (h₃ : homotopy (f ≫ b) 0)

include H₂ h₂ h₃

/--
If `A ⟶ B ⟶ C` is split exact, and `b' ≫ g` and `f ≫ b` are null-homotopic,
then so is `b' ≫ b`.

        B''
        ∣
        b'
        ↓
A - f → B - g → C
        ∣
        b
        ↓
        B'
-/
def comp_null_homotopic_of_row_split_exact : homotopy (b' ≫ b) 0 :=
begin
  haveI := λ i, (H₂ i).split_epi,
  haveI := λ i, (H₂ i).split_mono,
  have aux := λ i, (H₂ i).short_exact.3,
  let h₁' := (h₂.trans (homotopy.of_eq (comp_zero : 𝟙 _ ≫ 0 = 0).symm)).symm,
  let h₂' := (h₃.trans $ homotopy.of_eq (zero_comp : 0 ≫ 𝟙 _ = 0).symm),
  refine ((of_termwise_split_epi_homotopy h₁').symm.comp
    (of_termwise_split_mono_homotopy h₂')).trans (homotopy.of_eq _),
  apply hom.ext,
  apply funext,
  intro i,
  exact comp_eq_zero_of_exact (f.f i) (g.f i) (aux i)
    (congr_f ((of_termwise_split_epi_commutes h₁').trans comp_zero) i)
    (congr_f ((of_termwise_split_mono_commutes h₂').trans zero_comp) i)
end

end

def cone.termwise_split (i : ℤ) : splitting ((cone.in f).f i) ((cone.out f).f i) :=
{ iso := biprod.braiding _ _,
  comp_iso_eq_inl := by ext; simp [cone.in],
  iso_comp_snd_eq := by ext; simp [cone.out] }

@[simp] lemma cone.termwise_split_section (i : ℤ) :
  (cone.termwise_split f i).section = biprod.inl :=
by { delta splitting.section cone.termwise_split, ext; dsimp; simp }

@[simp] lemma cone.termwise_split_retraction (i : ℤ) :
  (cone.termwise_split f i).retraction = biprod.snd :=
by { delta splitting.retraction cone.termwise_split, dsimp, simp }

def cone_homotopy_equiv_aux (c : cone f ⟶ cone f) (h₁ : homotopy (cone.in f ≫ c) (cone.in f))
  (h₂ : homotopy (c ≫ cone.out f) (cone.out f)) : homotopy (𝟙 _) (2 • c - c ≫ c) :=
begin
  have : homotopy ((𝟙 _ - c) ≫ (𝟙 _ - c)) 0,
  { apply comp_null_homotopic_of_row_split_exact (cone.in f) (cone.out f) (cone.termwise_split f),
    { refine (homotopy.of_eq _).trans h₂.symm.equiv_sub_zero, simp },
    { refine (homotopy.of_eq _).trans h₁.symm.equiv_sub_zero, simp } },
  apply homotopy.equiv_sub_zero.symm _,
  refine (homotopy.of_eq _).trans this,
  simp [two_smul], abel,
end

local attribute [simp] preadditive.comp_nsmul preadditive.nsmul_comp

/--
If the following diagram commutes up to homotopy, then `c` is a homotopy equivalence
A - f → B ⟶ C(f) ⟶ A⟦1⟧
|       |      ∣       ∣
𝟙       𝟙      c       𝟙
↓       ↓      ∣       ∣
A - f → B ⟶ C(f) ⟶ A⟦1⟧
-/
def cone_homotopy_equiv (c : cone f ⟶ cone f) (h₁ : homotopy (cone.in f ≫ c) (cone.in f))
  (h₂ : homotopy (c ≫ cone.out f) (cone.out f)) : homotopy_equiv (cone f) (cone f) :=
{ hom := c,
  inv := ((2 • 𝟙 _) - c),
  homotopy_hom_inv_id := (homotopy.of_eq (by simp)).trans (cone_homotopy_equiv_aux f c h₁ h₂).symm,
  homotopy_inv_hom_id := (homotopy.of_eq (by simp)).trans (cone_homotopy_equiv_aux f c h₁ h₂).symm }

local notation `Q` := homotopy_category.quotient V (complex_shape.up ℤ)

lemma cone_triangleₕ_map_iso_of_id (φ : cone.triangleₕ f ⟶ cone.triangleₕ f)
  (h₁ : φ.hom₁ = 𝟙 _) (h₂ : φ.hom₂ = 𝟙 _) : is_iso φ.hom₃ :=
begin
  have e₂ := φ.comm₂,
  have e₃ := φ.comm₃,
  rw [h₂, category.id_comp] at e₂,
  rw [h₁, category_theory.functor.map_id, category.comp_id] at e₃,
  erw [← Q .image_preimage φ.hom₃, ← Q .map_comp] at e₂ e₃,
  convert is_iso.of_iso (homotopy_category.iso_of_homotopy_equiv
    (cone_homotopy_equiv _ _ (homotopy_category.homotopy_of_eq _ _ e₂)
    (homotopy_category.homotopy_of_eq _ _ e₃.symm))),
  exact (Q .image_preimage _).symm
end

open category_theory.triangulated

lemma cone.triangleₕ_is_iso {A' B' : cochain_complex V ℤ} {f : A ⟶ B} {f' : A' ⟶ B'}
  (φ : cone.triangleₕ f ⟶ cone.triangleₕ f') [is_iso φ.hom₁] [is_iso φ.hom₂] : is_iso φ :=
begin
  suffices : is_iso φ.hom₃,
  { exactI triangle_morphism_is_iso _ },
  have := φ.comm₁,
  dsimp at this,
  rw [← is_iso.eq_comp_inv, category.assoc, ← is_iso.inv_comp_eq,
    ← Q .image_preimage (inv φ.hom₁), ← Q .map_comp,
    ← Q .image_preimage (inv φ.hom₂), ← Q .map_comp] at this,
  let T := cone.triangleₕ_map (homotopy_category.homotopy_of_eq _ _ this).symm,
  haveI := cone_triangleₕ_map_iso_of_id _ (φ ≫ T) (by simp) (by simp),
  haveI := cone_triangleₕ_map_iso_of_id _ (T ≫ φ) (by simp) (by simp),
  haveI : epi φ.hom₃ := @@epi_of_epi _ (T.hom₃) (φ.hom₃) (show epi (T ≫ φ).hom₃, by apply_instance),
  use T.hom₃ ≫ inv (φ ≫ T).hom₃,
  split,
  { rw ← category.assoc, exact is_iso.hom_inv_id _ },
  { rw [← cancel_epi φ.hom₃, ← category.assoc, ← category.assoc, category.comp_id,
      category.assoc],
    exact is_iso.hom_inv_id_assoc (φ ≫ T).hom₃ _ }
end

instance : is_iso (from_termwise_split_mono_lift_triangleₕ f) :=
begin
  haveI : is_iso (from_termwise_split_mono_lift_triangleₕ f).hom₁,
  { delta from_termwise_split_mono_lift_triangleₕ, dsimp, apply_instance },
  haveI : is_iso (from_termwise_split_mono_lift_triangleₕ f).hom₂ :=
    is_iso.of_iso (homotopy_category.iso_of_homotopy_equiv
      (termwise_split_mono_factor_homotopy_equiv f)),
  apply cone.triangleₕ_is_iso,
end

-- move this
@[simp]
lemma cochain_complex_d_next (i : ℤ) (f : Π i j, A.X i ⟶ B.X j) :
  d_next i f = A.d i (i + 1) ≫ f (i + 1) i :=
by simp [d_next]

@[simp]
lemma cochain_complex_prev_d (i : ℤ) (f : Π i j, A.X i ⟶ B.X j) :
  prev_d i f = f i (i - 1) ≫ B.d (i - 1) i :=
by simp [prev_d]

@[simps]
def termwise_split_to_cone (h : ∀ i, splitting (f.f i) (g.f i)) :
  C ⟶ cone f :=
{ f := λ i, biprod.lift (-(connecting_hom f g h).f i) ((h i).section),
  comm' := begin
    rintro i j (rfl : i + 1 = j),
    haveI := λ i, (h i).split_epi,
    haveI := λ i, (h i).split_mono,
    ext,
    { dsimp [cone.d],
      rw ← cancel_epi (g.f _),
      { simp [g.comm, splitting.π_section_eq_id_sub_assoc] },
      { apply_instance } },
    { dsimp [cone.d],
      rw ← cancel_epi (g.f _),
      { simp [splitting.π_section_eq_id_sub_assoc, splitting.π_section_eq_id_sub] },
      { apply_instance } },
  end }

@[simps]
def comp_termwise_split_to_cone_homotopy (h : ∀ i, splitting (f.f i) (g.f i)) :
  homotopy (g ≫ termwise_split_to_cone f g h) (cone.in f) :=
{ hom := λ i j,
    if e : j + 1 = i then -(h i).retraction ≫ (A.X_eq_to_iso e).inv ≫ biprod.inl else 0,
  zero' := λ _ _ r, dif_neg r,
  comm := λ i, begin
    dsimp,
    simp only [dite_eq_ite, cochain_complex_prev_d, dif_pos, if_true, category.assoc, cone_d,
      category.id_comp, add_left_inj, sub_add_cancel, dif_ctx_congr, X_eq_to_iso_refl, cone.d,
      preadditive.comp_neg, eq_self_iff_true, cochain_complex_d_next, preadditive.neg_comp],
    ext,
    { simp [cone.in, splitting.π_section_eq_id_sub_assoc, ← sub_eq_add_neg,
      -retraction_X_eq_to_hom_assoc] },
    { simp [cone.in, splitting.retraction_ι_eq_id_sub, ← sub_eq_add_neg,
      -retraction_X_eq_to_hom_assoc] },
  end }

@[simps]
def cone_to_termwise_split (h : ∀ i, splitting (f.f i) (g.f i)) :
  cone f ⟶ C :=
{ f := λ i, biprod.snd ≫ g.f i,
  comm' := begin
    rintro i j (rfl : i + 1 = j),
    ext; simp [cone.d, (h _).comp_eq_zero],
  end }

@[simps]
def cone_to_termwise_split_comp_homotopy (h : ∀ i, splitting (f.f i) (g.f i)) :
  homotopy (cone_to_termwise_split f g h ≫ connecting_hom f g h) (-cone.out f) :=
{ hom := λ i j,
    if e : j + 1 = i then biprod.snd ≫ (h i).retraction ≫ (A.X_eq_to_iso e).inv else 0,
  zero' := λ _ _ r, dif_neg r,
  comm := begin
    intro i,
    dsimp,
    simp only [category.comp_id, dite_eq_ite, cochain_complex_prev_d, cone.out, dif_pos, if_true,
      add_left_inj, sub_add_cancel, cone.d, shift_d, dif_ctx_congr, preadditive.comp_neg,
      eq_self_iff_true, int.neg_one_pow_one, cochain_complex_d_next, one_zsmul,
      category.assoc, X_eq_to_iso_d, neg_neg, neg_smul, biprod.lift_snd_assoc,
      X_eq_to_iso_refl, cone_d, preadditive.neg_comp],
    ext; simp [splitting.π_section_eq_id_sub_assoc, sub_eq_add_neg],
  end }

def iso_cone_of_termwise_split_inv_hom_homotopy (h : ∀ i, splitting (f.f i) (g.f i)) :
  homotopy (cone_to_termwise_split f g h ≫ termwise_split_to_cone f g h) (𝟙 _) :=
{ hom := λ i j, if e : j + 1 = i then
    -biprod.snd ≫ (h i).retraction ≫ (A.X_eq_to_iso e).inv ≫ biprod.inl else 0,
  zero' := λ _ _ r, dif_neg r,
  comm := begin
    intro i,
    dsimp,
    simp only [category.comp_id, dite_eq_ite, cochain_complex_prev_d, dif_pos, if_true,
      category.id_comp, add_left_inj, sub_add_cancel, cone.d, dif_ctx_congr,
      eq_self_iff_true, cochain_complex_d_next, category.assoc, biprod.lift_snd_assoc,
      X_eq_to_iso_refl, cone_d],
    ext; -- This is simp [splitting.π_section_eq_id_sub_assoc, splitting.π_section_eq_id_sub]
      simp only [add_left_neg, add_zero, category.assoc, category.comp_id, exact.w, exact.w_assoc,
        biprod.inl_desc, biprod.inl_desc_assoc, biprod.inl_fst, biprod.inr_desc_assoc,
        biprod.inr_fst, biprod.inr_snd, biprod.inr_snd_assoc, biprod.lift_fst, biprod.lift_snd,
        biprod.lift_snd_assoc, comp_zero, zero_comp, preadditive.add_comp, preadditive.comp_add,
        preadditive.comp_neg, preadditive.neg_comp, preadditive.neg_comp, category.comp_id,
        splitting.ι_retraction_assoc, eq_self_iff_true, X_eq_to_iso_d, X_eq_to_iso_f_assoc,
        X_eq_to_iso_refl, X_eq_to_iso_trans, neg_neg, neg_zero, zero_add, neg_sub, hom.comm_assoc,
        splitting.π_section_eq_id_sub_assoc, splitting.π_section_eq_id_sub, category.id_comp,
        preadditive.sub_comp_assoc, hom.comm, preadditive.sub_comp, splitting.ι_retraction,
        exact_inl_snd];
      abel
  end }

@[simps]
def iso_cone_of_termwise_split (h : ∀ i, splitting (f.f i) (g.f i)) :
  triangleₕ_of_termwise_split f g h ≅
    (category_theory.triangulated.neg₃_functor _).obj (cone.triangleₕ f) :=
begin
  fapply mk_triangle_iso,
  exact iso.refl _,
  exact iso.refl _,
  refine ⟨Q .map (termwise_split_to_cone f g h), Q .map (cone_to_termwise_split f g h), _, _⟩,
  { dsimp, erw [← Q .map_comp, ← Q .map_id], congr, ext; dsimp, simp },
  { dsimp, erw [← Q .map_comp, ← Q .map_id], apply homotopy_category.eq_of_homotopy,
    apply iso_cone_of_termwise_split_inv_hom_homotopy },
  { exact (category.comp_id _).trans (category.id_comp _).symm },
  { dsimp, rw [← Q .map_comp, category.id_comp],
    apply homotopy_category.eq_of_homotopy, apply comp_termwise_split_to_cone_homotopy },
  { dsimp, rw [category_theory.functor.map_id, category.comp_id,
    ← Q .map_neg, ← Q .map_comp], congr, ext, simp [cone.out] }
end

instance : mono (termwise_split_mono_lift f) := mono_of_eval _

def termwise_split_of_termwise_split_mono [H : ∀ i, split_mono (f.f i)] (i : ℤ) :
  splitting (f.f i)
    ((@@homological_complex.normal_mono _ _ f (mono_of_eval _)).g.f i) :=
begin
  apply left_split.splitting,
  dsimp only [normal_mono, cokernel_complex_π],
  constructor,
  exact ⟨(H i).1, (H i).2⟩,
  exact abelian.exact_cokernel _,
end

/-- Every neg₃ of a cone triangle is isomorphic to some triangle associated to some
  termwise split sequence -/
def iso_termwise_split_of_cone :
      (category_theory.triangulated.neg₃_functor _).obj (cone.triangleₕ f) ≅
    triangleₕ_of_termwise_split (termwise_split_mono_lift f)
      (homological_complex.normal_mono (termwise_split_mono_lift f)).g
    (termwise_split_of_termwise_split_mono _) :=
functor.map_iso _ (as_iso $ from_termwise_split_mono_lift_triangleₕ f).symm ≪≫
  (iso_cone_of_termwise_split _ _ _).symm

-- Lemma 13.9.15. skipped

--move
@[simp, reassoc]
lemma biprod.map_desc {C : Type*} [category C] [has_zero_morphisms C]
  {X Y X' Y' Z : C} [has_binary_biproduct X Y] [has_binary_biproduct X' Y']
  (f : X ⟶ X') (g : Y ⟶ Y') (f' : X' ⟶ Z) (g' : Y' ⟶ Z) :
    biprod.map f g ≫ biprod.desc f' g' = biprod.desc (f ≫ f') (g ≫ g') :=
by { ext; simp }

@[simp, reassoc]
lemma biprod.lift_map {C : Type*} [category C] [has_zero_morphisms C]
  {W X Y X' Y' : C} [has_binary_biproduct X Y] [has_binary_biproduct X' Y']
  (f : X ⟶ X') (g : Y ⟶ Y') (f' : W ⟶ X) (g' : W ⟶ Y) :
    biprod.lift f' g' ≫ biprod.map f g = biprod.lift (f' ≫ f) (g' ≫ g) :=
by { ext; simp }

@[simps]
def biprod.map_iso {C : Type*} [category C] [has_zero_morphisms C]
  {X Y X' Y' : C} [has_binary_biproduct X Y] [has_binary_biproduct X' Y']
  (f : X ≅ X') (g : Y ≅ Y') : X ⊞ Y ≅ X' ⊞ Y' :=
⟨biprod.map f.hom g.hom, biprod.map f.inv g.inv, by ext; simp, by ext; simp⟩

@[simps]
def iso_connecting_hom_shift_cone (h : ∀ i, splitting (f.f i) (g.f i)) :
  B ≅ cone ((connecting_hom f g h)⟦(-1 : ℤ)⟧') :=
hom.iso_of_components (λ f, (h _).iso ≪≫ biprod.braiding _ _ ≪≫
  biprod.map_iso (C.X_eq_to_iso (by simp)) (A.X_eq_to_iso (by simp)))
begin
  haveI := λ i, (h i).split_epi,
  haveI := λ i, (h i).split_mono,
  rintro i j (rfl : i + 1 = j),
  dsimp [cone.d],
  rw ← cancel_epi (h i).iso.inv,
  simp only [category.comp_id, biprod.lift_map, neg_smul_neg, if_true, iso.inv_hom_id_assoc,
    add_left_inj, eq_self_iff_true, one_zsmul, category.assoc, neg_neg, neg_smul],
  ext; simp only [add_zero, category.assoc, exact.w_assoc, biprod.inl_fst_assoc,
    biprod.inr_fst_assoc, biprod.inr_snd_assoc, biprod.lift_desc, biprod.lift_fst,
    biprod.lift_snd, comp_zero, zero_comp, preadditive.comp_add, X_d_eq_to_iso, X_eq_to_iso_d,
    splitting.comp_iso_eq_inl_assoc, splitting.inl_comp_iso_eq_assoc,
    splitting.iso_comp_snd_eq_assoc, eq_self_iff_true, hom.comm_assoc, zero_add,
    splitting.iso_hom_fst_assoc, splitting.inr_iso_inv_assoc, exact_inl_snd],
  { rw ← cancel_epi (g.f _),
    simp only [category.id_comp, preadditive.sub_comp_assoc, (h _).comp_eq_zero_assoc,
      sub_zero, category.assoc, comp_zero, hom.comm, preadditive.sub_comp, limits.zero_comp,
      splitting.π_section_eq_id_sub_assoc, hom.comm_assoc],
    rw [← X_eq_to_iso_f, X_d_eq_to_iso_assoc],
    apply_instance },
  { rw ← cancel_epi (g.f _),
    simp only [category.comp_id, X_d_eq_to_iso, category.id_comp, preadditive.sub_comp_assoc,
      splitting.π_section_eq_id_sub_assoc, category.assoc, hom.comm, preadditive.sub_comp,
      splitting.ι_retraction],
    rw [← X_eq_to_iso_f_assoc, splitting.π_section_eq_id_sub_assoc],
    simp only [X_d_eq_to_iso_assoc, category.comp_id, hom.comm_assoc, retraction_X_eq_to_hom,
      category.id_comp, preadditive.sub_comp_assoc, X_eq_to_iso_d_assoc, splitting.ι_retraction,
      preadditive.comp_sub, hom.comm, preadditive.sub_comp, sub_right_inj, category.assoc],
    rw [← retraction_X_eq_to_hom_assoc, X_eq_to_iso_d],
    apply_instance }
end

lemma inv_rotate_iso_cone_triangle_comm₁ (h : ∀ i, splitting (f.f i) (g.f i)) :
  (triangle_of_termwise_split f g h).nonneg_inv_rotate.mor₁ ≫ (shift_shift_neg _ _).inv =
    𝟙 _ ≫ (cone.triangle ((connecting_hom f g h)⟦(-1 : ℤ)⟧')).mor₁ :=
by { ext, dsimp, simp, dsimp, simp }

lemma inv_rotate_iso_cone_triangle_comm₂ (h : ∀ i, splitting (f.f i) (g.f i)) :
  (triangle_of_termwise_split f g h).nonneg_inv_rotate.mor₂ ≫
    (iso_connecting_hom_shift_cone f g h).hom =
    (shift_shift_neg _ _).inv ≫ (cone.triangle ((connecting_hom f g h)⟦(-1 : ℤ)⟧')).mor₂ :=
by { ext; dsimp [cone.in]; simp }

lemma inv_rotate_iso_cone_triangle_comm₃ (h : ∀ i, splitting (f.f i) (g.f i)) :
  (triangle_of_termwise_split f g h).nonneg_inv_rotate.mor₃ ≫
    (𝟙 _)⟦(1 : ℤ)⟧' = (iso_connecting_hom_shift_cone f g h).hom ≫
      (cone.triangle ((connecting_hom f g h)⟦(-1 : ℤ)⟧')).mor₃ :=
by { ext, dsimp [cone.out], simpa }

def inv_rotate_iso_cone_triangle (h : ∀ i, splitting (f.f i) (g.f i)) :
  (triangle_of_termwise_split f g h).nonneg_inv_rotate ≅
    cone.triangle ((connecting_hom f g h)⟦(-1 : ℤ)⟧') :=
begin
  fapply mk_triangle_iso,
  exacts [iso.refl _, (shift_shift_neg _ _).symm, iso_connecting_hom_shift_cone f g h,
    inv_rotate_iso_cone_triangle_comm₁ _ _ _, inv_rotate_iso_cone_triangle_comm₂ _ _ _,
    inv_rotate_iso_cone_triangle_comm₃ f g h],
end

def triangle_of_termwise_split_cone_iso :
  triangle_of_termwise_split (cone.in f) (cone.out f) (cone.termwise_split f) ≅
    (cone.triangle f).nonneg_rotate :=
mk_triangle_iso (iso.refl _) (iso.refl _) (iso.refl _)
  (by { dsimp, simp }) (by { dsimp, simp }) (by { ext, dsimp [cone.d], simp })

end homological_complex

subset_name: curated


text:
\begin{document}
\noindent
{\Large  THE COSMOLOGICAL CONSTANT OF EMERGENT\\ SPACETIME IN THE NEWTONIAN APPROXIMATION}
\noindent

\vskip.5cm
\noindent
{\bf J.C. Castro-Palacio}$^{a}$, {\bf P. Fern\'andez de C\'ordoba}$^{b}$ and {\bf  J.M. Isidro}$^{c}$\\
Instituto Universitario de Matem\'atica Pura y Aplicada,\\ Universidad Polit\'ecnica de Valencia, Valencia 46022, Spain\\
${}^{a}${\tt juancas@upvnet.upv.es}, ${}^{b}${\tt pfernandez@mat.upv.es},\\
${}^{c}${\tt joissan@mat.upv.es}
\vskip.5cm
\noindent
\today
\vskip.5cm
\noindent
{\bf Abstract}  We present a simple quantum--mechanical estimate of the cosmological constant of a Newtonian Universe. We first mimic the dynamics of a Newtonian spacetime by means of a nonrelativistic quantum mechanics for the matter contents of the Universe (baryonic and dark)  within a fixed ({\it i.e.}\/, nondynamical) Euclidean spacetime. Then we identify an operator that plays, on the matter states, a role analogous to that played by the cosmological constant. Finally we prove that there exists a quantum state for the matter fields, in which the above mentioned operator has an expectation value equal to the cosmological constant of the given Newtonian Universe.

\section{Introduction}\label{einfuehrung}

\subsection{Goals}

While avoiding the sophistication of general relativity, Newtonian cosmology succeeds in capturing some essential physics of the Universe. In this letter we take advantage of this simplification in order to present a toy model of a Newtonian Universe, in which a certain repulsive force plays a role analogous to that played by the cosmological constant $\Lambda$ in general relativity.

In natural units one has the approximate value $\Lambda\simeq 10^{-122}$ \cite{PLANCK}. Therefore  $\Lambda^{-1}\simeq 10^{122}$, a number that comes surprisingly close to $S_{\rm max}/k_B\simeq 10^{123}$. Here $k_B$ denotes the Boltzmann constant, while $S_{\rm max}$ is the maximal entropy of the Universe allowed by the holographic principle \cite{THOOFT, SUSSKIND}. This approximate equality of two dimensionless quantities might be a coincidence, but it might also hide some deeper connection. In this paper we explore this latter possibility.

In refs. \cite{PADDY1, PADDY2}, a nonzero value of the cosmological constant has been argued to render the amount of cosmic information accessible to an eternal observer finite. This relation has allowed to determine the numerical value of the cosmological constant from the quantum structure of spacetime. Information is of course related to entropy, which seems to point towards the existence of some link between the two dimensionless numbers $\Lambda^{-1}\simeq 10^{122}$ and $S_{\rm max}/k_B\simeq 10^{123}$.

Of course one would like to be able to derive the above numbers from a full--fledged theory of quantum gravity.  More modestly, in refs.  \cite{CABRERA, NOI} we have obtained $S_{\rm max}/k_B\simeq 10^{123}$ using a finite--dimensional quantum--mechanical model\footnote{By this we mean the quantum theory of a {\it finite}\/ number of degrees of freedom, as opposed to a field theory.} of a Newtonian Universe. This strongly suggests that the cosmological constant $\Lambda$ must also be obtainable from the same model as in refs. \cite{CABRERA, NOI}. Carrying out this computation is one of the goals of the present paper.

Another goal is to establish a link between the operator that represents the cosmological constant $\Lambda$, on the one hand, and the entropy operator $S$ used in refs. \cite{CABRERA, NOI} to compute the number $S_{\rm max}/k_B\simeq 10^{123}$, on the other. For this we will resort, as already done in refs. \cite{CABRERA, NOI}, to some entropic notions concerning the emergent nature of spacetime put forward in ref. \cite{VERLINDE}.

\subsection{The cosmological constant as an operator}

The Newtonian gravitational attraction created by a unit point mass located at the origin is described by the attractive potential $-1/r$.  The derivative of the latter, $1/r^2$, is of course (minus) the Newtonian force. But one can also interpret $1/r^2$ as yet another potential, the corresponding  {\it repulsive}\/ force decaying like $1/r^3$. In this letter we take the point of view that the repulsive potential $1/r^2$ plays the role of a cosmological constant within a hypothetical Newtonian Universe. Arguments in favour of this interpretation are given below.

{}Following the steps of refs. \cite{CABRERA, NOI}, we will model the volume density of (baryonic and dark) mass in this toy Universe as being given by $\vert\psi({\bf x}, t)\vert^2$. Here $\psi({\bf x}, t)$ is a quantum wavefunction satisfying a 1--particle Schroedinger equation. The value of the mass $m$ present in this equation is the total (baryonic and dark) matter contents of the Universe; the mass $m_V$ enclosed by a volume $V$ equals $m_V=m\int_V{\rm d}^3x\vert\psi\vert^2$. By the correspondence principle, this quantum--mechanical model exhibits classical properties in the limit of large quantum numbers.  We will {\it a posteriori}\/ verify that the relevant quantum numbers involved do indeed fall within the semiclassical regime.

In the literature, the cosmological constant $\Lambda$ has adopted a number of different impersonations. To name but a few, in ref. \cite{RUSOS} is has appeared as the eigenvalue of a Sturm--Liouville problem, while in ref. \cite{BARROW} it has been regarded as a field. In our finite--dimensional  quantum--mechanical model an operator $\Omega$ and a state $\vert\psi\rangle$ can be identified, such that the expectation value $\langle\psi\vert\Omega\vert\psi\rangle$ will equal $\Lambda$. Specifically, the sought--for operator $\Omega$ is
\begin{equation}
\Omega=\frac{1}{r^2};
\label{landaerre}
\end{equation}
the state $\vert\psi\rangle$ will be specified presently. Up to a dimensionless multiplicative constant, the above form of $\Omega$ is dictated by symmetry (spatial isotropy) and by dimensional arguments: in standard ({\it i.e.}\/, nonnatural) units, $\Lambda$ has the dimensions of inverse length squared. We  see that $\Omega$ differs from the usual centrifugal potential $\hbar^2l(l+1)/(2mr^2)$ by multiplicative factors. However the centrifugal potential has a vanishing expectation value in the spherically symmetric $l=0$ states. This allows us to regard $\Omega$ as an analogue of the centrifugal force that however does not vanish in the $l=0$ states.

Based on the operator (\ref{landaerre}), our estimates for the cosmological constant $\Lambda$ are given by the dimensionless numbers $\Lambda_n$ defined as
\begin{equation}
\Lambda_n:=\frac{\hbar}{mH_0}\langle\psi_n\vert\Omega\vert\psi_n\rangle, \qquad n=1,2,\ldots,
\label{naddall}
\end{equation}
the best fit to the experimentally measured value of $\Lambda$ being obtained for a certain value of the quantum number $n$ in the semiclassical regime. Here the $\{\psi_n\}_{n=1}^{\infty}$ form a complete, orthonormal set of states in Hilbert space, $H_0$ is Hubble's constant, $m$ is the (baryonic and dark) mass of the observable Universe, and $R_0$ its radius. The dimensionless combination $\lambda:=\hbar/(mH_0R_0^2)$ will appear frequently; its numerical value is \cite{PLANCK}
\begin{equation}
\lambda:=\frac{\hbar}{mH_0R_0^2}=2.6\times 10^{-124}.
\label{kicktrumpout}
\end{equation}
The dimensionful constants $\hbar$, $m$ and $H_0$ are imposed on us by the requirement that $\Lambda$ be dimensionless (when expressed in natural units). Three such constants are needed, with the dimensions of action, mass and frequency; respectively Planck's constant, the (baryonic and dark) matter contents of the Universe, and Hubble's constant are natural choices to make.

Altogether, in units of the dimensionless parameter $\lambda$, our value $\Lambda_n$ for the cosmological constant $\Lambda$ is
\begin{equation}
\Lambda_n=\lambda R_0^2\langle\psi_n\vert\Omega\vert\psi_n\rangle, \qquad n=1,2,\ldots
\label{yoko}
\end{equation}
We will compute $\Lambda_n$ with respect to the eigenstates $\vert\psi_n\rangle$ of the free, 1--particle Hamiltonian operator
\begin{equation}
H_{\rm F}=-\frac{\hbar^2}{2m}\nabla^2,
\label{frei}
\end{equation}
which will be assumed to describe the matter contents of our hypothetical Newtonian Universe. We will find that the best fit of $\Lambda_n$ to the measured value of $\Lambda$  \cite{PERLMUTTER, RIESS} will occur for a certain value of $n$ in the semiclassical regime. However, in the first place, we need to justify our use of finite--dimensional quantum mechanics in the study of a Newtonian cosmological problem.

\section{Newtonian cosmology as a quantum mechanics}

In Newtonian cosmology (for a summary see, {\it e.g.}\/, ref. \cite{BONDI}) the Universe is regarded as being (a submanifold of) Euclidean $\mathbb{R}^3$. The gravitational potential $U$ satisfies the Poisson equation
\begin{equation}
\nabla^2U=4\pi G\rho.
\label{ztretre}
\end{equation}
The matter content (baryonic and dark) is modelled as an ideal fluid satisfying the continuity equation and the Euler equation,
\begin{equation}
\frac{\partial\rho}{\partial t}+\nabla\cdot\left(\rho{\bf v}\right)=0,\qquad \frac{\partial{\bf v}}{\partial t}+\left({\bf v}\cdot\nabla\right){\bf v}+\frac{1}{\rho}\nabla p-{\bf F}=0.
\label{zknoott}
\end{equation}
The cosmological principle requires that the velocity field ${\bf v}$ be everywhere proportional to the position vector ${\bf r}$. This requirement is equivalent to Hubble's law \cite{HUBBLE}, which can be described phenomenologically by the harmonic potential
\begin{equation}
U_{\rm Hubble}({\bf r})=-\frac{H_0^2}{2}{\bf r}^2.
\label{zpotenzi}
\end{equation}
Hubble's constant $H_0$ is a frequency; the negative sign implies that this potential is repulsive. Accordingly, $U_{\rm Hubble}$ satisfies the Poisson equation (\ref{ztretre}) with a {\it negative}\/ mass density.

Although not widely recognised, Schroedinger quantum mechanics can also be understood in terms of an ideal fluid, the {\it quantum probability fluid}\/. Following Madelung \cite{MADELUNG} one factorises the nonrelativistic wavefunction $\psi$ into amplitude and phase:
\begin{equation}
\psi=\exp\left(\frac{{\cal S}}{2k_B}+{\rm i}\frac{{\cal I}}{\hbar}\right).
\label{zbenouere}
\end{equation}
The amplitude $\exp({\cal S}/2k_B)$ is a real exponential; one can invoke Boltzmann's principle to regard  ${\cal S}$ as a Boltzmann entropy of the matter described by $\psi$. It will also be convenient to define a dimensionless Boltzmann entropy $S:={\cal S}/2k_B$. The phase $\exp({\rm i}{\cal I}/\hbar)$ is the complex exponential of the classical--mechanical action integral ${\cal I}$. Substituting the Ansatz (\ref{zbenouere}) into the Schroedinger equation for $\psi$, one arrives at a set of two equations. One of them is the continuity equation for the quantum probability fluid,
\begin{equation}
\frac{\partial S}{\partial t}+\frac{1}{m}\nabla S\cdot\nabla {\cal I}+\frac{1}{2m}\nabla^2{\cal I}=0,
\label{konntt}
\end{equation}
where
\begin{equation}
{\bf v}:=\frac{1}{m}\nabla {\cal I}, \qquad \rho={\rm e}^{2S}.
\label{zvanednie}
\end{equation}
The second equation obtained is known as the {\it quantum Hamilton--Jacobi equation}\/:
\begin{equation}
\frac{\partial {\cal I}}{\partial t}+\frac{1}{2m}(\nabla {\cal I})^2+V+{\cal Q}=0,
\label{zvabueelnv}
\end{equation}
where $V$ is the external potential present in the Schroedinger equation.\footnote{We recall that the dimensions of $U$ in (\ref{ztretre}) and (\ref{zpotenzi}) are velocity squared, whereas those of $V$ in (\ref{zvabueelnv}) are mass times velocity squared.} Above,
\begin{equation}
{\cal Q}:=-\frac{\hbar^2}{2m}\left[\left(\nabla S\right)^2+\nabla^2 S\right]
\label{zvebiyer}
\end{equation}
is known as the {\it quantum potential}\/ \cite{MATONE}. Indeed, in the limit when $\hbar\to 0$, the quantum potential vanishes, and (\ref{zvabueelnv}) reduces to the classical Hamilton--Jacobi equation.

In order to be able to interpret quantum mechanics as an Euler fluid we need to derive an Euler equation for the quantum probability fluid. This is achieved by taking the gradient of  Eq. (\ref{zvabueelnv}):
\begin{equation}
\frac{\partial{\bf v}}{\partial t}+\left({\bf v}\cdot\nabla\right){\bf v}+\frac{1}{m}\nabla {\cal Q}+\frac{1}{m}\nabla V=0.
\label{kblm}
\end{equation}
Comparison between Eqs. (\ref{kblm}) and (\ref{zknoott}) produces a bijective correspondence between the quantum probability fluid and the cosmological fluid. According to this correspondence, Newtonian cosmology can be regarded in either one of two equivalent descriptions:
\begin{equation}
\begin{tabular}{| c | c | c|}\hline
& Euler &  Madelung  \\ \hline
fluid density & $\rho$ & $\exp(2S)$   \\ \hline
velocity field & ${\bf v}$ & $\nabla{\cal I}/m$   \\ \hline
fluid pressure & $\nabla p/\rho$ & $\nabla{\cal Q}/m$   \\ \hline
force per unit mass & ${\bf F}$ & $-\nabla V/m$   \\ \hline
\end{tabular}
\label{tabulauno}
\end{equation}
Which suggests that, {\it given the cosmological fluid in the Newtonian approximation, we use nonrelativistic quantum mechanics as an equivalent description thereof}\/.

We would like to add that, beyond Newtonian cosmology, the dark Universe has also found an interesting description as a cosmological fluid in refs. \cite{BOLOGNA1, BOLOGNA2, BOLOGNA3}.

\section{Computing $\Lambda$}\label{trumpburro}

The free Hamiltonian (\ref{frei}) admits  the spherical waves
\begin{equation}
\psi_{\kappa 00}(r,\theta,\phi)=\frac{1}{\sqrt{4\pi R_0}}\frac{1}{r}\exp\left({\rm i}\kappa r\right), \qquad\kappa\in\mathbb{R}
\label{iggn}
\end{equation}
as eigenfunctions. They are normalised within a sphere of radius $R_0$ (the radius of the observable Universe); $\vert\kappa\vert$ is the modulus of the linear momentum; the angular quantum numbers $l,m$ have been set to zero as demanded by the cosmological principle. For regularity of the wavefunction at the origin $r=0$ we will consider the normalised linear combination of the states (\ref{iggn}) given by
\begin{equation}
\psi_n(r)=\frac{1}{\sqrt{2\pi R_0}}\frac{1}{r}\sin\left(\frac{n\pi}{R_0} r\right), \qquad n=1,2,\ldots
\label{psiene}
\end{equation}
where the boundary condition $\psi(R_0)=0$ has been imposed. One readily finds the expectation value of the operator (\ref{landaerre}):
\begin{equation}
\langle\psi_n\vert\Omega\vert\psi_n\rangle=\frac{2\pi n}{R_0^2}{\rm Si}\left(2n\pi\right),\qquad n=1,2,\ldots
\label{sekko}
\end{equation}
where ${\rm Si}(x)=\int_0^x{\rm d}t\sin(t)/t$ \cite{LEBEDEV}. By Eq. (\ref{sekko}) in (\ref{yoko}) we arrive at the estimates $\Lambda_n$ for the cosmological constant $\Lambda$:
\begin{equation}
\Lambda_n=\lambda f(n),\qquad f(n):=2n\pi\,{\rm Si}\left(2n\pi\right), \qquad n=1,2,\ldots
\label{stoptrump}
\end{equation}
Evaluating $f(n)$ we can tabulate the first few values of $\Lambda_n$:
\begin{equation}
\begin{tabular}{| c | c | c|}\hline
$\Lambda_n$ & in units of $\lambda$ &  in natural units  \\ \hline
$n=1$ & $8.9$ & $2.3\times 10^{-123}$   \\ \hline
$n=2$ & $18.8$ & $4.9\times 10^{-123}$   \\ \hline
$n=3$ & $28.6$ & $7.4\times 10^{-123}$ \\ \hline
$n=4$ & $38.5$ & $1.0\times 10^{-122}$ \\ \hline
$n=5$ & $48.4$ & $1.3\times 10^{-122}$ \\ \hline
$n=6$ & $58.2$ & $1.5\times10^{-122}$ \\ \hline
$n=7$ & $68.1$ & $1.8\times 10^{-122}$ \\ \hline
$n=8$ & $78.0$ & $2.0\times 10^{-122}$ \\ \hline
$n=9$ & $87.8$ & $2.3\times 10^{-122}$ \\ \hline
$n=10$ & $97.7$ & $2.5\times 10^{-122}$ \\ \hline
$n=11$ & $107.6$ & $2.8\times 10^{-122}$ \\ \hline
$n=12$ & $117.4$ & $3.0\times 10^{-122}$ \\ \hline
\end{tabular}
\label{tabulados}
\end{equation}
They are in excellent agreement with the measured value of $\Lambda$, the best fit being around $n=11$, well inside the semiclassical regime as announced. As we let $n\to\infty$ we find
\begin{equation}
\langle\psi_n\vert\Omega\vert\psi_n\rangle\simeq\frac{n\pi^2}{R_0^2},\qquad\Lambda_n\simeq\lambda\pi^2n.
\label{gadde}
\end{equation}

\section{The cosmological constant operator as the inverse to the entropy operator}

\subsection{Emergent spacetime}

In  a Newtonian Universe, the area measured by $r^2$ has been argued to be proportional to the entropy within the volume enclosed by the given area. This point has been discussed at length in ref. \cite{VERLINDE}, where an entropic concept for the emergent nature of spacetime has been put forward.

The operator $r^2$ has played a key role in our computation of the number $S_{\rm max}/k_B\simeq 10^{123}$ in refs. \cite{CABRERA, NOI}. Specifically, the holographic bound $S_{\rm max}/k_B\simeq 10^{123}$ has been achieved as the expectation value of the operator $S=k_BmH_0 r^2/\hbar$ in a certain quantum eigenstate of the Hamiltonian (\ref{frei}). Modulo the physical constants $k_B$ $m$, $H_0$ and $\hbar$, the entropy operator used in refs. \cite{CABRERA, NOI} is the inverse operator to $1/r^2$ used here.

Therefore entropy and the cosmological constant are mutually inverse, not just as numbers as mentioned in section \ref{einfuehrung}, but also as quantum--mechanical operators.  The explanation for the approximate equality between the dimensionless numbers $\Lambda^{-1}\simeq 10^{122}$ and $S_{\rm max}/k_B\simeq 10^{123}$ lies in the deeper fact that {\it the corresponding quantum--mechanical operators are mutually inverse}\/.

Now the operator $\Omega=1/r^{2}$ becomes singular at $r=0$. Below we explore the consequences of this singularity in more detail. As we will see, one surprising consequence of the regularisation of this singularity will be the natural appearance of a quantum of length.

\subsection{Regularisation}\label{hadd}

Consider the coefficients $c_n$ of the Fourier--Bessel expansion of $\Omega=1/r^2$ in terms of Bessel functions \cite{LEBEDEV}:
\begin{equation}
c_n=\frac{2}{[R_0J'_{p}(z_{p}(n))]^2}\int_0^{R_0}J_{p}\left(\frac{z_{p}(n)}{R_0}r\right)\frac{{\rm d}r}{r},\qquad n=1,2,\ldots
\label{samschweber}
\end{equation}
Here $J'_p(x)$ denotes the derivative of the Bessel function $J_p(x)$ and $z_{p}(n)$ denotes the positive zeroes of the latter; the value of $p$ is specific to the precise Hamiltonian considered ($p=1/2$ for the Hamiltonian (\ref{frei})).  As will be proved below, it turns out that our $\Lambda_n$ of Eq. (\ref{yoko}) are proportional to the Fourier--Bessel coefficients $c_n$ in the limit when $n\to\infty$.

{}From a knowledge of the $c_n$ one may construct the formal series
\begin{equation}
\sum_{n=1}^{\infty}c_nJ_{p}\left(\frac{z_{p}(n)}{R_0}r\right).
\label{pentwicklung}
\end{equation}
Unfortunately the function $1/r^2$ on $(0,R_0)$ does not satisfy the conditions required for the series (\ref{pentwicklung}) to converge to the function $1/r^2$ on $(0,R_0)$ \cite{LEBEDEV}. However this does not deprive the coefficients $c_n$ of their meaning, since Eq. (\ref{samschweber}) make sense {\it per se}\/. Moreover, the cosmological constant  being relevant only at astronomical scales, $\Lambda$ does not affect the short--range physics. One could then introduce an ultraviolet cutoff $\epsilon>0$ and consider the function $1/r^2$ on $(\epsilon, R_0)$, where it does satisfy the requisite conditions for the series (\ref{pentwicklung}) to converge to $1/r^2$. The integrals in (\ref{samschweber}) would now extend over the interval $(\epsilon, R_0)$. Whichever interpretation one chooses (either to ignore convergence issues or to enforce convergence through an ultraviolet cutoff), the fact remains that, {\it in the semiclassical limit, the Fourier--Bessel coefficients of $1/r^2$ are proportional to the expectation values  of $1/r^2$}\/, as we establish next.

The complete orthonormal system of radial states (\ref{psiene}) can be recast in terms of Bessel functions as
\begin{equation}
\psi_n(r)=\frac{\sqrt{n\pi}}{2R_0}\frac{1}{\sqrt{r}}J_{\frac{1}{2}}\left(\frac{n\pi}{R_0}r\right),\quad n=1,2,\ldots
\label{eijenn}
\end{equation}
Thus setting $p=1/2$ and $z_{1/2}(n)=n\pi$, the Fourier--Bessel coefficients  (\ref{samschweber}) now read
\begin{equation}
c_n=\frac{2}{[R_0J'_{1/2}(n\pi)]^2}\int_0^{R_0}J_{\frac{1}{2}}\left(\frac{n\pi}{R_0}r\right)\frac{{\rm d}r}{r}=\frac{4n\pi^2}{R_0^2}C\left(\sqrt{2n}\right),
\label{schweber}
\end{equation}
where $C(z)=\int_0^z\cos\left(\pi t^2/2\right){\rm d}t$ \cite{LEBEDEV}. In the limit $n\to\infty$ we have
\begin{equation}
c_n\simeq \frac{2n\pi^2}{R_0^2}.
\label{adieu}
\end{equation}
Comparing Eqs. (\ref{adieu}) and (\ref{gadde}) we observe that, in the semiclassical limit, the Fourier--Bessel coefficients  of $1/r^2$ are indeed proportional to $\langle\psi_n\vert\Omega\vert\psi_n\rangle$ as announced.

{}Finally we repeat the above calculations without imposing a boundary condition at $r=R_0$. In particular this implies that the wavefunctions (\ref{iggn}) are permitted, even though they are singular at $r=0$. We have
\begin{equation}
\langle\psi_{\kappa}\vert \Omega\vert\psi_{\kappa}\rangle=\frac{1}{R_0}\int_0^{R_0}\frac{{\rm d}r}{r^2}
\label{avignon}
\end{equation}
This integral diverges at its lower limit; this is a consequence of the singular behaviour, at $r=0$, of both the wavefunction $\psi_{\kappa}$ and the operator $\Omega$. We regularise the integral (\ref{avignon}) by simply dropping the infinite contribution coming from its lower limit and find a regularised expectation value
\begin{equation}
\langle\psi_{\kappa}\vert \Omega\vert\psi_{\kappa}\rangle_{\rm reg}=-\frac{1}{R_0^2}.
\label{reku}
\end{equation}
While the operator $\Omega$ is nonnegative, a surprising minus sign appears on the right--hand side; this is a consequence of the regularisation.\footnote{This is not unsual. A well--known example is the $\zeta$--function regularisation of the divergent sum of positive integers $\sum_{n=1}^{\infty}n$, which yields the {\it negative}\/ value $-1/12$ \cite{ELIZALDE}.} With the regularised integral (\ref{reku}) we return to Eq. (\ref{naddall}) and, changing the sign,  find the dimensionless value
\begin{equation}
\langle\Lambda\rangle_{\rm reg}=-\frac{\hbar}{mH_0}\langle\Omega\rangle_{\rm reg}=\frac{\hbar}{mH_0R_0^2},
\label{rkki}
\end{equation}
in perfect agreement with our previous result (\ref{kicktrumpout}).

The above regularisation procedure may appear somewaht {\it ad hoc}\/, but in fact it is not. It is known in the literature under the dignified name of  Hadamard regularisation \cite{BLANCHET}, a popular choice when regularising  gravitational models. In what follows we briefly summarise the Hadamard regularisation in order to provide an alternative derivation of our Eq. (\ref{reku}). Given $x\in(a,b)$ and a function $f(t)$ sufficiently differentiable at $t=x$, consider the divergent integral
\begin{equation}
\int_a^b\frac{f(t)}{(t-x)^2}{\rm d}t.
\label{cochy}
\end{equation}
Then the Hadamard {\it partie finie}\/ of (\ref{cochy}), denoted by an ${\cal H}$ in front,  is defined by
\begin{equation}
{\cal H}\int_a^b\frac{f(t)}{(t-x)^2}{\rm d}t
\label{hadamard}
\end{equation}
$$
=\lim_{\epsilon\to 0^+}\left[\int_a^{x-\epsilon}\frac{f(t)}{(t-x)^2}{\rm d}t+\int_{x+\epsilon}^b\frac{f(t)}{(t-x)^2}{\rm d}t-\frac{f(x-\epsilon)+f(x+\epsilon)}{\epsilon}\right]
$$
In the case at hand we rewrite our divergent integral (\ref{avignon}) as
\begin{equation}
\langle\psi_{\kappa}\vert \Omega\vert\psi_{\kappa}\rangle=\frac{1}{2R_0}\int_{-R_0}^{R_0}\frac{{\rm d}r}{r^2}
\label{surlepontdavignon}
\end{equation}
in order to identify $a=-R_0$, $b=R_0$, $x=0$, $f(t)=1$. Applying Eq. (\ref{hadamard}) one readily verifies that
\begin{equation}
{\cal H}\int_{-R_0}^{R_0}\frac{{\rm d}r}{r^2}=-\frac{2}{R_0}.
\label{reggu}
\end{equation}
{}Finally Eqs. (\ref{surlepontdavignon}) and (\ref{reggu}) yield back our former result (\ref{reku}). We conclude that the ultraviolet cutoff $\epsilon>0$ mentioned previously is nothing but Hadamard regularisation.

\section{Discussion}

We have presented a nonrelativistic, quantum--mechanical model of a hypothetical Newtonian Universe, in which an operator can be identified that plays a role analogous to a cosmological constant. Indeed the expectation value of this operator in a certain basis of quantum states yields a value that lies close to the measured value of the cosmological constant.

Admittedly, our toy model is not a theory of quantum spacetime; it contains one adjustable parameter, the quantum number $n$. All this notwithstanding, the close equality of the two dimensionless quantities $\Lambda^{-1}\simeq 10^{122}$ and $S_{\rm max}/k_B\simeq 10^{123}$ has a very simple explanation in our framework. Namely, the value $\Lambda^{-1}\simeq 10^{122}$ arises as the (inverse of the) expectation value of the operator $1/r^2$, while the $S_{\rm max}/k_B\simeq 10^{123}$ arises as the expectation value of $r^2$. Both expectation values are taken within the {\it same}\/ quantum--mechanical model. Moreover, the Hadamard regularisation used in section \ref{hadd}, seen to be equivalent to the inclusion of a cutoff $\epsilon$ in coordinate space, can be regarded as an indication of the existence of a quantum of length $\epsilon$. Thus the requirement of {\it finiteness}\/ of the cosmological constant leads naturally to the existence of a quantum of length.

Our result for $\Lambda$ depends on the specific choice of a complete set of orthonormal vectors $\left\{\vert\psi_n\rangle\right\}_{n=1}^{\infty}$ for 1--particle states; it also depends on the quantum number $n$. We have established that, for a given choice of orthonormal vectors, the best fit of $\Lambda_n$ to the measured value of $\Lambda$ occurs for a certain value of $n$ in the semiclassical regime. Of course, different Hamiltonians will lead to different choices for the set $\left\{\vert\psi_n\rangle\right\}_{n=1}^{\infty}$, and correspondingly to different values of $\Lambda_n$. In previous work by some of the present authors \cite{CABRERA, NOI, FINSTER}  we have modelled the Hubble expansion of a Newtonian Universe by means of an inverse oscillator \cite{PADDY3}
\begin{equation}
H_{\rm H}=H_{\rm F}-\frac{k_{\rm eff}r^2}{2},\qquad k_{\rm eff}=mH_0^2.
\label{jabel}
\end{equation}
In upcoming work we propose to use the Hamiltonian (\ref{jabel}) in order to refine our present estimate for the cosmological constant of a Newtonian Universe.

\vskip0.5cm
\noindent
{\bf Acknowledgements} This research was supported by grant no. RTI2018-102256-B-I00 (Spain).


TITLE: Mergers and ultrafilters
QUESTION [0 upvotes]: F - filter over I.
Please, prove, F ultrafilter <=> when $\forall$
X, Y $\subseteq$ I, if X $\notin$ F, Y $\notin$ F, $\Rightarrow$ X $\cup$ Y $\notin$ F.

REPLY [2 votes]: Hint: If $\cal F$ is an ultrafilter, pick $X,Y\notin\cal F$ and use the fact that their complements are in $\cal F$ and it is closed under intersections; in the other direction, if $\cal F$ is not an ultrafilter there is some $X$ such that $X,I\setminus X\notin\cal F$. Use these two sets to contradict the statement you have on the RHS.


TITLE: What is the $\int_{-1}^{1} (4t^4 - 4t^2 - 1) e^{-{(t^2 -1)}^2}dt$?
QUESTION [3 upvotes]: I tried doing this by substitution
$-((t^2 -1)^2) = u$
So $-4t(t^2 -1)dt = du$
but I don't know what to do with the "-1" in
$(4t^4 - 4t^2 -1) = (4t^2(t^2 -1) -1)$

REPLY [3 votes]: HINT 1:
$$\dfrac{d(te^{f(t)})}{dt}=e^{f(t)}(1+tf'(t))$$
HINT 2:
$$\dfrac{d(t^2-1)^2}{dt}=(4t^3-4t)$$

SPOLIER ALERT Scroll over the highlighted area to reveal the solution

We have the integral $$\int_{-1}^{1}(4t^4-4t^2-1)e^{-(t^2-1)^2}\,dt=\int_{-1}^{1}(4t^4-4t^2)e^{-(t^2-1)^2}\,dt-\int_{-1}^{1} e^{-(t^2-1)^2}\,dt \tag 1$$For the first integral in $(1)$ we integrate by parts letting $u=-t$ and $v=e^{-(t^2-1)^2}$.  Then, integrating by parts reveals that $$\int_{-1}^{1}(4t^4-4t^2)e^{-(t^2-1)^2}\,dt=\left.\left(-te^{-(t-1)^2}\right)\right|_{-1}^{1}+\int_{-1}^{1}e^{-(t-1)^2}\,dt \tag 2$$Substituting the right-hand of $(2)$ into the right-hand side $(1)$, we obtain $$\int_{-1}^{1}(4t^4-4t^2-1)e^{-(t^2-1)^2}\,dt=\left.\left(-te^{-(t-1)^2}\right)\right|_{-1}^{1}=-2$$


TITLE: Curvature calculation of the ellipse at the end of its axes
QUESTION [1 upvotes]: Calculate the curvature of the ellipse (of which the minor axis is b and the major axis is a) at the end of each axes!

REPLY [2 votes]: Here's a geometric construction for the radius of curvature at point $P$ of an ellipse with foci $A$ and $B$.

Construct the bisector $n$ of $\angle APB$, which is the normal at $P$.

Construct on ray $n$ points $H$ and $K$, such that $PH$ and $PK$ are the diameters of the circles tangent to the ellipse at $P$ and passing through $A$ and $B$ respectively (note that $\angle PAH=\angle PBK=90°$).

The radius of curvature is the harmonic mean of $PH$ and $PK$.

PROOF.
Let $P'$ be a point on the ellipse near to $P$ and let normal lines at $P$ and $P'$ meet at $C$. If we set
$$
\alpha=\angle PAP',\quad \beta=\angle PBP',\quad \theta=\angle PCP',
$$
then by angle chasing it is easy to find that
$$
2\theta=\alpha+\beta.
$$
Consider now the circle through $APP'$, let $d_A$ be its diameter and $a$ its arc $PP'$ subtended by $\alpha$: we have then $a=\alpha d_A$. We can repeat the same reasoning for the circles through $BPP'$ and $CPP'$, with diameters $d_B$ and $d_C$, and arcs: $b=\beta d_B$, $c=\theta d_C$. Obtaining $\alpha$, $\beta$ and $\theta$ from these equalities, and plugging them into the above equation gives then:
$$
2{c\over d_C}={a\over d_A}+{b\over d_B},
$$
which can be rearranged as:
$$
{1\over d_C}={1\over2}\left({a/c\over d_A}+{b/c\over d_B}\right).
$$
In the limit $P'\to P$, the circles through $APP'$ and $BPP'$ tend to the circles tangent to the ellipse at $P$ and passing through $A$ and $B$ respectively, while $C$ tends to the center of the osculating circle at $P$. Hence $d_C$ tends to the radius of curvature $\rho$ at $P$, while $d_A$ and $d_B$ tend to $PH$ and $PK$ defined above. In addition, both $a/c$ and $b/c$ tend to $1$ as $P'\to P$. The above equation implies then:
$$
{1\over \rho}={1\over2}\left({1\over PH}+{1\over PK}\right),
$$
as it was to be proved.

The same argument can be repeated for a hyperbola and a parabola, leading to
$$
{1\over \rho}={1\over2}\left|{1\over PH}-{1\over PK}\right|
\quad\text{and}\quad
\rho=2PH
$$
respectively. A detailed explanation for the parabola can be found here.


TITLE: Using truth tables to evaluate an argument and provide counterexamples.
QUESTION [1 upvotes]: So, I have been given an two compound conditional statements to use as premises with the aim of reaching a conditional conclusion. I need to determine the validity of this argument. Truth tables are somewhat confusing for me, but this is my best effort at figuring this problem out:
$$\begin{array}{c|c|c||c|c|c|c|c|c}
J & K & L & 1^{st} Prem: J\to(K\to L) & 2^{nd} Prem: K\to(J\to L) & Concl: (J \lor K)\to L\\\hline
F & F & F & T & T & T \\\hline
F & F & T & T & T & T \\\hline
F & T & F & T & T & F \\\hline
F & T & T & T & T & T \\\hline
T & F & F & T & T & F \\\hline
T & F & T & T & T & T \\\hline
T & T & F & F & F & F \\\hline
T & T & T & T & T & T \\\hline
\end{array}$$
From what I can tell, this argument is invalid because there are two instances where both premises are true but the conclusion is false. I need to come up with a counterexample and I am not sure where to begin

REPLY [1 votes]: You can substitute anything in for J, K, and L, so long as the truth values of your statements match the assigned values in the row where the premises are both true and the conclusion is false. If you use line 3, pick any statements for J, K, and L, where those statements are J (false), K (true), and L (false). The statements you use can be anything. The statements you choose do not have to relate to each other or even be about the same topic since the validity of the argument is not related to anything other than the truth values of the premises/conclusion. It is best to use well-known truths or falsehoods. The guy above said to use Bob is an adult male, bob is a bachelor, etc. I don't know who Bob is so I have no way to determine the truth value of a statement like "Bob is a bachelor.' However, everyone who is reading this proof will know that 'All humans are animals' is true, or that 'All odd numbers are divisible by 2' is false.. Using well known truths or falsehoods will give a much stronger counter-example. Instead of saying Bob is unmarried(since we have no way to verify this), use something that is a well-known truth. Something like
J = "all odd numbers are evenly divisible by 2"(which is well known to be false)
K = "all humans are animals" (which is well known to be true)
L = "all snakes are mammals" (which is well known to be false)...
These 3 statements aren't even related and it does not matter for a good counterexample. All that matters is that the atomic statements you choose for J, K and L are chosen so that their truth value matches the truth values in your line 3, which causes it to be the case that using them causes 2 true premises and a false conclusion. The fact that the argument itself allows for an opportunity for us to assign statements that give us true premises and false conclusion shows it is invalid- and that's exactly the point of a counter-argument. Hope this helps.
I will also point out that the truth table in the original post is not complete. You have to put a T or F under each logical operator and each atomic statement in your table. Each box therefore requires 2 truth values in this example. One for the main logical operator and one for the atomic statement(in parentheses).


TITLE: How to prove this sequence is unbounded?
QUESTION [1 upvotes]: Let $a_{n} = \dfrac{7n^{3} - 3n^{4} -1}{4n^{2} + 3}$
How to show this sequence is unbounded without using limits?
Well I know that I need to show that it unbounded from bottom or above.
I choose bottom, so I need to show that $\forall M \exists n \Rightarrow a_{n}>M$
What is the method? Can someone show me? Thanks!

REPLY [0 votes]: First, note the denominator is always positive, so
$$\frac{7n^3-3n^4-1}{4n^2+3}<0\iff 7n^3-3n^4-1<0\iff -3n^3\left(n-7\right)<1\iff$$
$$3n^3(n-7)>-1$$
and the last inequality is clearly true for $\;n\ge7\;$, and thus the sequence is bounded above, but
$$\frac{7n^3-3n^4-1}{4n^2+3}\le\frac{-3n^4+7n^3}{n^2}=-3n^2+7n$$
which, I believe, is much easier to prove it is unbounded below.


TITLE: Solve $\ln(1+t) = t/(1+t)$
QUESTION [0 upvotes]: How to solve
$$
 \ln(1+t) = \frac{t}{1+t}?
$$
By inspection I know that $t = 0$ is the only solution, but how to prove that?

REPLY [8 votes]: $$
 g(t) = \ln(1+t) - \frac{t}{1+t} , \ \ t>-1
$$
$$
 g'(t)=\frac{t}{(1+t)^2}
$$
Thus $g(0)=0$ and $g$is increasing on $(0,\infty )$ and decreasing on $(-1 , 0)$, so there can be no other roots in $(-1 , \infty)$.

REPLY [2 votes]: Let $x = 1 + t \to t = x - 1$, and consider: $f(x) = xlnx - x + 1$ on $(0,\infty)$. We have:
$f'(x) = lnx + 1 - 1 + 0 = lnx > 0$ if $x > 1$, and $< 0$, if $0 < x < 1$. Thus if $x > 1$, $f(x) > f(1) = 0 \to g(x) = \dfrac{f(x)}{x} > 0$, and the equation has no solution. Similarly when $0 < x < 1$, $f(x) > f(1) = 0$, so $g(x) = \dfrac{f(x)}{x} > 0$, and the equation again has no solution. So $x = 1$, and $1 + t = 1 \to t = 0$ is the only solution.

REPLY [1 votes]: For $t\in\mathbb{R}$, the function $f(t)=\log(1+t)-\dfrac{t}{1+t}$ is increasing on $[0, \infty)$ and decreasing on $(-1, 0]$. The derivative is $f'(t)=\dfrac{t}{(1+t)^2}$.

$\lim\limits_{t\to\infty}f(t)=\infty$.
$\lim\limits_{t\to-1^+}f(t)=\infty$.
$f'(0) = 0$.
$f(0) = 0$.

So, we have a proof that the only zero of $f(t)$ is when $t=0$. Have we?


TITLE: how should i solve this fration of complex numbers?
QUESTION [1 upvotes]: hi everybody i have a question i can't solve
$$\left|\frac{Z-W}{1-\overline ZW}\right|=1$$
the question says the above is true ,use it and prove $|Z|=1$ or $|W|=1$
i have tried putting $Z = x +iy$ and $W= a +ib$  and done some math works but it doesnt get to what question wants
thanks alot

REPLY [4 votes]: $|a+b|^{2}=|a|^{2}+|b|^{2}+2\Re \overset {-} a b$ for any two complex numbers $a$ and $b$. Since $|Z-W|^{2}=|1-\overset {-} Z W|^{2}$ we get $(1-|Z|^{2})(1-|W|^{2})=0$ after some simplifications. Hence $|Z|=1$ or $|W|=1$.


TITLE: Show using inequality of means that $a\cdot n \cdot \frac{1}{n} \le a^2n^2+\frac{1}{n^2}$
QUESTION [0 upvotes]: Show using inequality of means that for $a>0$ and $n\in\mathbb{N}$: $$a\cdot n \cdot \frac{1}{n} \le a^2n^2+\frac{1}{n^2}$$

I'm sure it's not that complicated, but I'm probably missing something..
This is actually a small part of a proof which I want to understand.

REPLY [2 votes]: This is a simple case of AM-GM and we can do even better:
$$a^2n^2+\frac1{n^2}\ge2\sqrt{a^2n^2/n^2}=2a$$
Alternatively,
$$0\le\left(an-\frac1n\right)^2=a^2n^2-2a+\frac1{n^2}\implies a^2+\frac1{n^2}\ge 2a$$

REPLY [2 votes]: In fact the given inequality is sharp. It follows from AM-GM inequality:
$\dfrac{1}{2}\left(a^2n^2+\dfrac{1}{n^2}\right) \geq \sqrt{a^2n^2.\dfrac{1}{n^2}}=a.n.\dfrac{1}{n}$


TITLE: Introduction to Real Analysis (Proof Based Course) Spivak vs Baby Rudin?
QUESTION [3 upvotes]: I'm a second year math major and I don't know which is the right book for me?
I hope that only someone who studied both or has a strong background in analysis attempts to answer my question because random answers are shared pretty much everywhere.
Please note that I only know: elementary set theory aka discrete mathematics and calculus
Thanks!

REPLY [1 votes]: I think Baby Rudin is a better introduction. I would advise that and there's also an excellent video series by Professor Su of Harvey Mudd College with an accompanying website called Rudinium which has over 200 problems to go along with the videos.
The video quality isn't great but I think he's an excellent instructor.


TITLE: Whether these induced topologies are comparable?
QUESTION [2 upvotes]: $$\|x\|_1=\sum_{i=1}^{n} |x_i|$$ and $$\|x\|_2=(\sum_{i=1}^{n}|x_i|^2)^{1\over 2}$$ these two norm induce topologies on $\mathbb{R}^n$, I want to know whether they are comparable?

REPLY [3 votes]: As @Kahen said, it is a standard result that all norms on a finite-dimensional real vector space are equivalent, however, in this particular case, it can be deduced with some ease (the following inequalities are immediate):
$$|x_i|\leq \left(\sum_{i=1}^n |x_i|^2\right)^{1/2}$$
and
$$\sum_{i=1}^n |x_i|^2\leq \left(\sum_{i=1}^n |x_i|\right)^2$$

REPLY [0 votes]: Neighbourhoods in the first topology are (unions of) arbitrarily small N-spheres, those in the second are (unions of) arbitrarily small N-cubes. It's obvious that every sphere contains a cube, which is enough for comparability; but also that every cube contains a sphere, so we have equivalence.