TITLE: Finding distribution of X
QUESTION [0 upvotes]: We have X=Z if U<=0.5 and X=-Z if U>0.5 where Z is a standard normal variable and U is a uniform random variable (0,1).
I want to find the distribution of X. I am mainly unsure of how to approach this because of the inclusion of the uniform r.v.
Noting that Z and U are independent.
I know that Fu(u) = u for 0<u<1.
Am I correct in stating the following:
Fx(x) = P(X<=x) = P(Z<=x) = Then it would be the integral from 0 to 0.5 of the standard normal pdf?
Fx(x) = P(X<=x) = P(-Z<=x)= P(Z>=-x) = 1-P(Z<=-x) = 1 - (negative integral from 0.5 to 1 of the standard normal pdf)
Any feedback would be appreciated.

REPLY [0 votes]: $$P(X \leq x)=P(X \leq x, U\leq \frac1 2)+P(X \leq x, U> \frac1 2)$$ $$=P(Z \leq x, U\leq \frac1 2)+P(-Z \leq x, U> \frac1 2).$$
By independence this becomes $P(Z \leq x) P( U\leq \frac1 2)+P(-Z \leq x) P(U>\frac1 2)$ Can you continue?


text:
(*  Title:       One procedure
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for 1 Procedure"

theory PLang imports Main begin

subsection\<open>The language\<close>

typedecl state

type_synonym bexp = "state \<Rightarrow> bool"

datatype com = Do "(state \<Rightarrow> state set)"
             | Semi  com com            ("_; _"  [60, 60] 10)
             | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
             | While bexp com           ("WHILE _ DO _"  60)
             | CALL
             | Local "(state \<Rightarrow> state)" com "(state \<Rightarrow> state \<Rightarrow> state)"
               ("LOCAL _; _; _" [0,0,60] 60)

text\<open>\noindent There is only one parameterless procedure in the program. Hence
@{term CALL} does not even need to mention the procedure name. There
is no separate syntax for procedure declarations. Instead we declare a HOL
constant that represents the body of the one procedure in the program.\<close>

consts body :: com

text\<open>\noindent
As before, command execution is described by transitions
\<open>s -c\<rightarrow> t\<close>. The only new rule is the one for @{term CALL} ---
it requires no comment:\<close>

inductive
  exec :: "state \<Rightarrow> com \<Rightarrow> state \<Rightarrow> bool"  ("_/ -_\<rightarrow>/ _" [50,0,50] 50)
where
    Do:     "t \<in> f s \<Longrightarrow> s -Do f\<rightarrow> t"

  | Semi:   "\<lbrakk> s0 -c1\<rightarrow> s1; s1 -c2\<rightarrow> s2 \<rbrakk>
            \<Longrightarrow> s0 -c1;c2\<rightarrow> s2"

  | IfTrue:  "\<lbrakk> b s;  s -c1\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t"
  | IfFalse: "\<lbrakk> \<not>b s; s -c2\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t"

  | WhileFalse: "\<not>b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s"
  | WhileTrue:  "\<lbrakk> b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u \<rbrakk>
                \<Longrightarrow> s -WHILE b DO c\<rightarrow> u"

  | "s -body\<rightarrow> t \<Longrightarrow> s -CALL\<rightarrow> t"

  | Local: "f s -c\<rightarrow> t \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t"

lemma [iff]: "(s -Do f\<rightarrow> t) = (t \<in> f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d\<rightarrow> u) = (\<exists>t. s -c\<rightarrow> t \<and> t -d\<rightarrow> u)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d\<rightarrow> t) =
              (s -if b s then c else d\<rightarrow> t)"
apply(rule iffI)
 apply(auto elim: exec.cases intro:exec.intros)
apply(auto intro:exec.intros split:if_split_asm)
done

lemma unfold_while:
 "(s -WHILE b DO c\<rightarrow> u) =
  (s -IF b THEN c;WHILE b DO c ELSE Do(\<lambda>s. {s})\<rightarrow> u)"
by(auto elim: exec.cases intro:exec.intros split:if_split_asm)

lemma [iff]: "(s -CALL\<rightarrow> t) = (s -body\<rightarrow> t)"
by(blast elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -LOCAL f; c; g\<rightarrow> u) = (\<exists>t. f s -c\<rightarrow> t \<and> u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

lemma [simp]: "\<not>b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s"
by(fast intro:exec.intros)

lemma WhileI: "\<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u"
by(fastforce elim:exec.WhileTrue)
(*>*)

text\<open>This semantics turns out not to be fine-grained
enough. The soundness proof for the Hoare logic below proceeds by
induction on the call depth during execution. To make this work we
define a second semantics \mbox{\<open>s -c-n\<rightarrow> t\<close>} which expresses that the
execution uses at most @{term n} nested procedure invocations, where
@{term n} is a natural number. The rules are straightforward: @{term
n} is just passed around, except for procedure calls, where it is
decremented:\<close>

inductive
  execn :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"   ("_/ -_-_\<rightarrow>/ _" [50,0,0,50] 50)
where
  "t \<in> f s \<Longrightarrow> s -Do f-n\<rightarrow> t"

| "\<lbrakk> s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 \<rbrakk> \<Longrightarrow> s0 -c1;c2-n\<rightarrow> s2"

| "\<lbrakk>  b s; s -c1-n\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2-n\<rightarrow> t"
| "\<lbrakk> \<not>b s; s -c2-n\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2-n\<rightarrow> t"

| (*<*)WhileFalse:(*>*)"\<not>b s \<Longrightarrow> s -WHILE b DO c-n\<rightarrow> s"
| (*<*)WhileTrue:(*>*)"\<lbrakk>b s; s -c-n\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c-n\<rightarrow> u"

| "s -body-n\<rightarrow> t \<Longrightarrow> s -CALL-Suc n\<rightarrow> t"

| "f s -c-n\<rightarrow> t \<Longrightarrow> s -LOCAL f; c; g-n\<rightarrow> g s t"

lemma [iff]: "(s -Do f-n\<rightarrow> t) = (t \<in> f s)"
by(auto elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -c1;c2-n\<rightarrow> u) = (\<exists>t. s -c1-n\<rightarrow> t \<and> t -c2-n\<rightarrow> u)"
by(best elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -IF b THEN c ELSE d-n\<rightarrow> t) =
              (s -if b s then c else d-n\<rightarrow> t)"
apply auto
apply(blast elim: execn.cases intro:execn.intros)+
done

lemma [iff]: "(s -CALL- 0\<rightarrow> t) = False"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -CALL-Suc n\<rightarrow> t) = (s -body-n\<rightarrow> t)"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -LOCAL f; c; g-n\<rightarrow> u) = (\<exists>t. f s -c-n\<rightarrow> t \<and> u = g s t)"
by(auto elim: execn.cases intro:execn.intros)

text\<open>\noindent By induction on @{prop"s -c-m\<rightarrow> t"} we show
monotonicity w.r.t.\ the call depth:\<close>

lemma exec_mono[rule_format]: "s -c-m\<rightarrow> t \<Longrightarrow> \<forall>n. m \<le> n \<longrightarrow> s -c-n\<rightarrow> t"
apply(erule execn.induct)
         apply(blast)
        apply(blast)
       apply(simp)
      apply(simp)
     apply(simp add:execn.intros)
    apply(blast intro:execn.intros)
   apply(clarify)
   apply(rename_tac m)
   apply(case_tac m)
    apply simp
   apply simp
  apply blast
done

text\<open>\noindent With the help of this lemma we prove the expected
relationship between the two semantics:\<close>

lemma exec_iff_execn: "(s -c\<rightarrow> t) = (\<exists>n. s -c-n\<rightarrow> t)"
apply(rule iffI)
apply(erule exec.induct)
           apply blast
          apply clarify
          apply(rename_tac m n)
          apply(rule_tac x = "max m n" in exI)
          apply(fastforce intro:exec.intros exec_mono simp add:max_def)
         apply fastforce
        apply fastforce
       apply(blast intro:execn.intros)
      apply clarify
      apply(rename_tac m n)
      apply(rule_tac x = "max m n" in exI)
      apply(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
     apply blast
    apply blast
apply(erule exE, erule execn.induct)
         apply blast
        apply blast
       apply fastforce
      apply fastforce
     apply(erule exec.WhileFalse)
    apply(blast intro: exec.intros)
   apply blast
  apply blast
done

lemma while_lemma[rule_format]:
"s -w-n\<rightarrow> t \<Longrightarrow> \<forall>b c. w = WHILE b DO c \<and> P s \<and>
                    (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not>b t"
apply(erule execn.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
 "\<lbrakk>s -WHILE b DO c-n\<rightarrow> t; P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s' \<rbrakk> \<Longrightarrow> P s'\<rbrakk>
  \<Longrightarrow> P t \<and> \<not>b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end

subset_name: curated


TITLE: Exponentiation in Lambda Calculus
QUESTION [4 upvotes]: I just need a double check.
Some recitation notes say:
EXP $= λmn.m$ $($MUL $n)$ $\underline{1}$.
The notes also say:  EXP $= λmn.nm$
I think I found an inconsistency and would like someone to double check if that's appropriate for this site:
Let $\underline{m}$ and $\underline{n}$ be Church numerals representing natural numbers $n$ and $m$ respectively. More specifically, $\underline{m} = λfx.f^mx$, where $f^m$ is the $m$-fold composition of $f$ and likewise for $\underline{n}$. When applied to EXP as EXP $\underline{m}$ $\underline{n}$ I get inconsistent results:

With EXP $= λmn.m$ $($MUL $n)$ $\underline{1}$

EXP $\underline{m}$ $\underline{n} = \underline{n^m}$.

In contrast, with EXP $= λmn.nm$

EXP $\underline{m}$ $\underline{n} = \underline{m^n}$

Using an Online Lambad Calculus interpreter, I confirmed that with EXP $= λmn.nm$, EXP $\underline{2}$ $\underline{3} = \underline{2^3} = \underline{8}$
This is the input into the online interpreter that corresponds to $(λmn.nm)$ $\underline{2}$ $\underline{3}$:
(lambda m n.n m) (lambda f x. f(f x)) (lambda f x.f(f(f x)))

REPLY [4 votes]: I agree with you it's confuing here as referenced here:

$exp~ m~ n = m^n = nm$

which gives the lambda expression,
$exp \equiv \lambda m.\lambda n.nm$

So its second definition means $m^n$ after applying to $m$ and $n$ consecutively. While as explained above your first definition of EXP:

exponentiation is iterated multiplication:

So you need to read the first definition as $m$ should be at the exponent position and $n$ should be at the base position after applying to $m$ and $n$ consecutively. So there's no inconsistency here, just need to be careful about how to read and interpret these 2 similar but subtly different definitions...


TITLE: Probability that given weight is on the heavier side of a balance
QUESTION [2 upvotes]: Assume we have 6 balls weighting 101, 102, 103, 104, 105 and 106 in kg. If we randomly pick 3 balls and place them on one side of the scale and the other 3 left are placed on the other side of the scale. What is the probability that the ball weighting 106 kg is on the heavier side?

REPLY [4 votes]: The problem is same as considering the weights $1,2,3,4,5,6$ instead.
There are $\dfrac{6!}{3!3!2!}=10$ ways to divide $6$ distinct objects into two groups of threes. One way, quick enough, is to list out the ten pairs of triples and see for how many cases $6$ belongs to the group with larger sum.
A yet shorter way is to consider the sum $1+2+3+4+5+6=21$. $6$ belongs to heavier side, when sum of three weights including $6$ is more than $21/2=10.5$. Unfavorable cases are only two : $(6,1,2)$ and $(6,1,3)$.
Number of favorable events is $10-2=8$ and required probability is $8/10$.


TITLE: $f\in L^1 [0,1]$, condition for integrability of $g =\int_x^1t^{-1} f(t)dt$
QUESTION [3 upvotes]: In my continuing studies towards an upcoming exam, I have run across a number of problems similar to the following, and would appreciate 1) some guidance on how to approach such problems in general and 2) how to solve this one in particular.
Let $f \in L^1[0,1]$ and define $g(x) = \int_{[x,1]} \frac{f(t)}{t} dt$. Show that $g \in L^1[0,1]$ and $\int_{[0,1]} g = \int_{[0,1]} f$.
I suspect the use of Tonelli's theorem is required, so I wrote
\begin{align*}
\int_{[0,1]} |g| &= \int_{[0,1]} \left| \int_{[x,1]} \frac{f(t)}{t} dt \right| dx \\
&= \int_{[0,1]} \left| \int_{[0,1]} \chi_{[x,1]} \frac{f(t)}{t} dt \right| dx \\
&= \int_{[0,1]} \left| \frac{f(t)}{t} \int_{[0,1]} \chi_{[x,1]} dx \right| dt
\end{align*}
However, I'm not sure if this is even a productive direction. Thanks for any assistance.

REPLY [3 votes]: Since it should hold for all $f \in L^1([0,\,1])$, it would in particular hold for positive $f$, so you must be able to move the absolute value into the inner integral. That yields
$$\begin{align}
\int_{[0,1]} \lvert g(x)\rvert\,dx &= \int_{[0,1]}\left\lvert \int_{[x,1]} \frac{f(t)}{t}\,dt\right\rvert\, dx\\
&\leqslant \int_0^1 \int_x^1 \frac{\lvert f(t)\rvert}{t}\,dt\,dx\\
&= \int_0^1\int_0^t \frac{\lvert f(t)\rvert}{t}\,dx\,dt\\
&= \int_0^1 \left(\int_0^t dx\right)\frac{\lvert f(t)\rvert}{t}\,dt\\
&= \int_0^1 \lvert f(t)\rvert\, dt.
\end{align}$$
Changing the order of integration is no problem because the integrand is measurable and non-negative.
The same computation without the absolute value yields (we now know that Fubini's theorem can be applied)
$$\int_0^1 g(x)\,dx = \int_0^1 f(t)\,dt.$$


TITLE: Calculating the error in the resolving time?
QUESTION [0 upvotes]: In a Geiger counter experiment, I am asked to calculate the error in the resolving time and what I have is the resolving time from the formula
$$T_r = \frac{(R_1+R_2-R_{12})}{(2R_1R_2)}$$
where $R_1$ is the count rate for the right half of the source, $R_2$ is the count rate for the left half of the source and $R_{12}$ is the count rate for both right and left halfs . And I also have the true count rate which I got from the formula $\displaystyle{R= \frac{R_o}{(1-R_oT_r)}}$
So any hint how to get the error in the resolving time ? Thank you in advance

REPLY [0 votes]: Your should consider the measured rates to be independent Poisson-distributed variables, meaning that their standard deviation scales with $\sqrt{N}$ where $N$ is the number of observed counts.
Then use the normal equations for combining errors when adding / dividing quantities.
UPDATE as @Farcher pointed out, there is a correlation between values in the numerator and denominator; you can avoid this by simply rewriting your expression as
$$T_R = \frac12\left(\frac{1}{R_1}+\frac{1}{R_2}-\frac{R_{12}}{R_1 R_2}\right)$$
in which case you no longer have correlated errors in your expression.


TITLE: Orthogonal polynomials/functions on the interval [0,1] but with same weight as Gegenbauer polynomials
QUESTION [4 upvotes]: I am looking for an othogonal basis of functions over the interval $[0,1]$ with weight function $(1-x^2)^{\alpha-1/2}$. Gegenbauer polynomials are frustratingly close to what I need, but they are defined over the interval $[-1,1]$, and a change of variables ends up changing the weight function.
None of the orthogonal polynomial families I have looked at (Chebyshev, Gegenbauer, Legendre, Laguerre, Jacobi, Hermite) have this property.
Does anyone know of a family that does? Suggestions for references that may point the way would also be very helpful.
Thanks!

REPLY [0 votes]: The even (degree) Gegenbauer polynomials $C_{2n}^{(\alpha )}$, $n=0,1,2,\ldots$ form an orthogonal basis for the space of square integrable functions over [0,1] with respect to the weight function $(1-x^2)^{\alpha -1/2}$, and so do the odd (degree) Gegenbauer polynomials $C_{2n+1}^{(\alpha )}$, $n=0,1,2,\ldots$


TITLE: Inverse of $x\cdot\sin(x)$
QUESTION [2 upvotes]: In the function
$$f(x) = x\cdot\sin(x)$$
every codomain value $y$ occurrs infinitely many times. So, in principle, there are "inverse" functions $f^{-1}$ such that
$$f^{-1}(y)=x \mbox{ and } f(x)=y$$
for every $y \in \mathbb{R}$.
(I know that there is no ONE inverse function in the traditional sense (therefore, the "quotes"), but I'm looking for a function that has the above and below properties which are fairly close to an inverse.)
I'm particularly interested in inverse values $f^{-1}(y)$ that are closest to zero. That is, for values of $y$ below the maximum of the smallest "sine hill", I'd like to get the respective $x$ value on the zero-facing side of that hill, for values larger than that, but smaller than the maximum of the second hill, the function should jump to the zero-facing side of the second hill and so on. (Only looking for positive $x$ values.)
There are probably no closed forms for that (but maybe there are partial closed forms that can be defined interval-wise in some way)? Numerical solutions would also suffice - or any other ideas.

REPLY [0 votes]: Strictly speaking, an 'inverse' trigonometric function like $\arcsin$ is not a proper inverse of $\sin:\mathbb{R}\rightarrow[-1,1]$. This is because $\sin$ is not injective over the domain $\mathbb{R}$. In order to define $\arcsin$, you have to decide on a 'principal value', such as the range $[-\pi/2,\pi/2]$.
The same is true of your function $f$, which is also not injective. Indeed you have specified a principal value, but it is good to remember that $f^{-1}$ is not a true inverse, despite its notation.
The function $f^{-1}$, defined using these principal values, does exist (is well-defined) and will be piecewise smooth. You can justify this using the inverse function theorem. There is no closed form for $f^{-1}$, but you can work out numerical values for it using a scheme such as interval bisection or Newton's method.


TITLE: Possible wrong answer to Spivak calculus chapter on graphs of functions
QUESTION [0 upvotes]: In problem #17-v of Spivak's Calculus (3rd edition, chapter 4) the reader is asked to draw the graph of the function $f(x)= [1/x]$, where $[\ldotp]$ is the greatest integer function. I did the problem and then checked the answer, but the answer provided in the manual seems to be wrong. I have attached a link to the image of the answer provided in the manual: https://imgur.com/a/jN4LW4H.
Is the answer wrong?

REPLY [1 votes]: Yes, it does appear to be wrong if it is the plain ‘greatest integer’ function and not something more special. The problem is where $x<0$.
Although $\frac{1}{x} \to 0 $ as $x \to -\infty$, since $\frac{1}{x} < 0$ for all $x < 0$, the lines drawn on the left hand side of a plot of $y = f(x)$ should always be at $y = -1$ or below.
The floor function $\lfloor x \rfloor$ gives the greatest integer less than or equal to $x$ and so clearly it will be $0$ only if $x \geq 0$.


TITLE: Show that $f_n(x) = \frac{x^2}{n}$ for $x \in \mathbb{R}$ does not converge uniformly towards $0$ for $n \rightarrow \infty$
QUESTION [2 upvotes]: Consider the sequence of functions
$$
f_n(x) = \frac{x^2}{n}
$$
for $x \in \mathbb{R}$
I have shown that $f_n(x)$ converges pointwise towards $0$ for $n \rightarrow \infty$ but I am not sure whether my attempt for showing that it does not converge uniformly towards $0$ for $n \rightarrow \infty$ is correct. Do you mind verifying?
By negation we have that $f_n(x)$ does not converge towards $0$ for $n \rightarrow \infty$ if
$$\exists \epsilon > 0 \forall n \in \mathbb{N} \exists x \in \mathbb{R} \exists n \in \mathbb{N}: n \geq N \Rightarrow |\frac{x^2}{n}| \geq \epsilon$$
Let $\epsilon = 1$. Then for all $n \in \mathbb{N}$ we can find a $x \in \mathbb{R}$ such that for $n \geq N$ that $|x^2/n| \geq 1$. Can I then just pick $x = n^{1/2}$ so we have that
$$
|x^2/n| = |(n^{1/2})^2/n| = |n/n| = 1 \geq 1
$$
which means that $f_n(x)$ does not converge uniformly towards $0$ for $n \rightarrow \infty$. Is this ok?

REPLY [1 votes]: You've got a typo in your negation of uniform convergence.
$f_n$ converges uniformly to $0$ if for all $\epsilon$ there exists some $N$ such that for all $x, n,$ we have $n \geq N \implies |f_n(x)| < \epsilon.$
Assuming a suitable replacement of $n$ with $N,$ you negated all of this correctly except the last implication. The negation of "$A \implies B$" is not " $A \implies \neg B,$" as both are true when $A$ is false. Instead, the negation is "$A$ and $\neg B.$"
That exchanged $n$ and $N$ have lead to another small mistake - you're allowed to pick both $x,n$ depending on $N,$ such that $n > N$ and $|x^2/n| \geq 1.$ You've wisely picked $x = \sqrt N,$ how will you pick $n$?


TITLE: Find the limit $\lim_{x \to 0} \left( 1 + \sin \left( \frac 3 x \right) \right)^x$
QUESTION [2 upvotes]: What is the answer to the limit?
$$\lim_{x \to 0} \left( 1 + \sin \left( \frac 3 x \right) \right)^x$$
The book's answer shows that $e^3$ while I keep getting $e^0$. I used the estimation
$$\lim_{x \to 0} x \ln x \le \lim_{x \to 0} x \ln \left( 1 + \sin \left( \frac 3 x \right) \right) \le 0$$

REPLY [1 votes]: Pick a fixed  $\alpha\geq 0$. Let $a=e^{-2\pi\alpha/3}$.
Pick $u_n\in(0,\pi/2)$ so that $\sin u_n =1-a^n$.
Then define $x_n=\frac{3}{2n\pi - u_n}$.
Then $1+\sin(3/x_n)=a^n$, and $(a^n)^x=e^{-\frac{2\pi n\alpha}{2n\pi+u_n}}$
So $x_n\to 0$, and $\frac{2\pi n}{2n\pi+u_n}\to 1$, so
$$\left(1+\sin\left(\frac3{x_n}\right)\right)^{x_n}\to e^{-\alpha}$$
So the above limit cannot exist. It has all of $[0,1]$ as limit points.


TITLE: Does $x(t) = \exp\left(\frac{t}{t-1}\right)\cdot\theta(1-t)$ solve $\dot{x}\cdot(1-t)^2+x=0,\,\,x(0)=1$?
QUESTION [1 upvotes]: Does $x(t) = \exp\left(\frac{t}{t-1}\right)\cdot\theta(1-t)$ solve $\dot{x}\cdot(1-t)^2+x=0,\,\,x(0)=1$ with $\theta(t)$ the standard unitary step/Heaviside function
$$\theta(t) := \begin{cases} 0 & x\leq 0 \\ 1 & x > 0. \end{cases}$$
I know beforehand that $y(t) =\exp\left(\frac{t}{t-1}\right)$ solves $\dot{y}\cdot(1-t)^2+y=0,\,\,y(0)=1$, and I want to know if the same differential equation sustained as a finite-duration solution the cropped version $x(t)$.
If not, please explain which differential equation will be solved by $x(t)$ on the whole real line.
My attempts
Through Wolfram-Alpha I take the derivative of $x(t)$ and it looks it match the differential equation, except at one zero-measure point where a Dirac's Delta function rises, but because this term has the form $f(1-t)\delta(1-t)$ when multiplied by $(1-t)^2$ on the diff. eq., I believe lies under the property $x\cdot\delta(x) = 0$ so indeed $x(t)$ is solving the differential equation.
Since this system is not an autonoums ODE, it is different from the problems analyzed by V. T. Haimo:  Finite Time Differential Equations and Finite Time Controllers, so I don't know how to apply here was is shown on the papers. Maybe someone with a better background on differential equations could explain how to figure out if indeed the differential equation stand a finite duration solution (these are the only related papers I have found so far).
But given I already know that $y(t)$ solves the irrestricted diff. eq., which also has the trivial solution $y(t)=0$, I believe that since $x(t)$ achieves zero "smoothly" there are no reasons to discard it as a solution... which is quite interestimg thinking about Uniqueness of solutions which should stand every Lipschitz ODE, so I guess the differential equation is not a Lipschitz ODE please confirm this explaining why.

REPLY [2 votes]: Your equation is not an ODE at $t=1$, so as ODE it only has solutions for $t<1$ and for $t>1$.
However, as all these solutions have limit $0$ at $t=1$, you can combine any solution left of $t=1$ with any solution right of $t=1$ to get a continuous function that solves the given equation.
But no such combination is "The" solution of this equation. Your case is also such a combination, with the zero solution for $t>1$.