text:
Riemann-Lebesgue Lemma, Jordan's, and Dini's Theorem Review

# Riemann-Lebesgue Lemma, Jordan's, and Dini's Theorem Review

We will now review some of the recent material regarding the Riemann-Lebesgue Lemma, Jordan's Theorem, and Dini's Theorem.

• We began on the Lebesgue Integrable Functions with Arbitrarily Small Integrable Terms page by looking at a very nice theorem which said that if $f$ is Lebesgue integrable on an interval $I$ then for all $\epsilon > 0$ there exists upper functions $u^*$ and $v^*$ on $I$ for which $f = u^* - v^*$, $v^*$ is nonnegative almost everywhere on $I$, and:
(1)
\begin{align} \quad \int_I v^*(x) \: dx < \epsilon \end{align}
• We also saw that if $f$ is Lebesgue integrable on an interval $I$ then for all $\epsilon > 0$ there exists a Lebesgue integrable function $g$ on $I$, and a step function $s$ on $I$ for which $f = g + s$ and:
(2)
\begin{align} \quad \int_I \mid g(x) \mid \: dx < \epsilon \end{align}
• To summarize these two very important results, if $f \in L(I)$ then we can firstly find an upper function representation $f = u^* - v*$ of $f$ whose difference contains a upper function $v^*$ that is nonnegative almost everyone on $I$ and whose Lebesgue integral over $I$ can be made arbitrarily small. We can also find a Lebesgue integrable function $g$ and a step function $s$ where $f = g + s$ and such that the Lebesgue integral of $g$ over $I$ can be made arbitrarily small.
• On The Riemann-Lebesgue Lemma page we used the result above to prove the very important Riemann-Lebesgue lemma which says that if $f \in L(I)$ and $\beta \in \mathbb{R}$ then:
(3)
\begin{align} \quad \lim_{\alpha \to \infty} \int_I f(t) \sin (\alpha t + \beta) \: dt = 0 \end{align}
• We proved this by first showing that it is true for step functions and then wrote $f = g + s$ where $g \in L(I)$, $s \in S(I)$, and where $\displaystyle{\int_I \mid g(x) \mid \: dx}$ was made arbitrarily small from the previous result.
• As a simple corollary to the Riemann-Lebesgue lemma we obtained the following identities by setting $\beta = 0$ and $\displaystyle{\beta = \frac{\pi}{2}}$ respectively for any $f \in L(I)$:
(4)
\begin{align} \quad \lim_{\alpha \to \infty} \int_I f(t) \sin \alpha t \: dt = 0 \end{align}
(5)
\begin{align} \quad \lim_{\alpha \to \infty} \int_I f(t) \cos \alpha t \: dt = 0 \end{align}
• On the Bonnet's Theorem page we looked at an important result. It said that if $f$ is an increasing function on $[a, b]$, $g$ is continuous on $[a, b]$, and $A, B \in \mathbb{R}$ are such that $A \leq f(a+) \leq f(b-) \leq B$ then there exists an $x_0 \in [a, b]$ for which:
(6)
\begin{align} \quad \int_a^b f(x) g(x) \: dx = A \int_a^{x_0} g(x) \: dx + B \int_{x_0}^b g(x) \: dx \end{align}
• We then proved Bonnet's theorem as a consequence for when $f$ is an increasing function on $[a, b]$, $g$ is continuous on $[a, b]$, $B \in \mathbb{R}$ is such that $f(b-) \leq B$, and $f(x) \geq 0$ for all $x \in [a, b]$, which says that there then exists an $x_0 \in [a, b]$ for which:
(7)
\begin{align} \quad \int_a^b f(x) g(x) \: dx = B \int_{x_0}^b g(x) \: dx \end{align}
• Here we applied the previous theorem by setting $A = 0 \leq f(a+)$ (since $f(x) \geq 0$ for all $x \in [a, b]$).
• On the Dirichlet Integrals page we looked at a special type of integral. We said that a Dirichlet Integral is an integral of the following form (for $g \in L([0, b])$ and $b > 0$):
(8)
\begin{align} \quad \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt \end{align}
• Assuming that $g(0+) = \lim_{t \to 0+} g(t)$ exists, we began to investigate the nature of the limit $\displaystyle{\lim_{\alpha \to \infty} \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt}$. We saw that if $g$ is a constant function on $[0, b]$ then:
(9)
\begin{align} \quad \lim_{\alpha \to \infty} \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt = \frac{\pi}{2} \cdot g(0+) \quad \Leftrightarrow \quad \lim_{\alpha \to \infty} \frac{2}{\pi} \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt = g(0+) \quad (*) \end{align}
• We then began to look at sufficient conditions which allowed for the property $(*)$ to hold. On the Jordan's Theorem for Dirichlet Integrals page we proved that if $g$ is of bounded variation on $[0, b]$ for some $b > 0$ then $\displaystyle{\lim_{\alpha \to \infty} \frac{2}{\pi} \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt = g(0+)}$.
• On the Dini's Theorem for Dirichlet Integrals page we looked at another sufficient condition which said that if $g \in L([0, b])$ for some $b > 0$, $g(0+)$ exists, and the Lebesgue integral $\displaystyle{\int_0^b \frac{g(t) - g(0+)}{t} \: dt}$ exists, then $\displaystyle{\lim_{\alpha \to \infty} \frac{2}{\pi} \int_0^b g(t) \frac{\sin \alpha t}{t} \: dt = g(0+)}$.


text:
# Convex analysis

A 3-dimensional convex polytope. Convex analysis includes not only the study of convex subsets of Euclidean spaces but also the study of convex functions on abstract spaces.

Convex analysis is the branch of mathematics devoted to the study of properties of convex functions and convex sets, often with applications in convex minimization, a subdomain of optimization theory.

## Convex sets

Main article: Convex set

A convex set is a set CX, for some vector space X, such that for any x, yC and λ ∈ [0, 1] then[1]

$\lambda x + (1 - \lambda)y \in C$.

## Convex functions

Main article: Convex function

A convex function is any extended real-valued function f : XR ∪ {±∞} which satisfies Jensen's inequality, i.e. for any x, yX and any λ ∈ [0, 1] then

$f(\lambda x + (1 - \lambda)y) \leq \lambda f(x) + (1-\lambda) f(y)$.[1]

Equivalently, a convex function is any (extended) real valued function such that its epigraph

$\left\{(x,r) \in X \times \mathbf{R}: f(x) \leq r \right\}$

is a convex set.[1]

## Convex conjugate

Main article: Convex conjugate

The convex conjugate of an extended real-valued (not necessarily convex) function f : XR ∪ {±∞} is f* : X*R ∪ {±∞} where X* is the dual space of X, and[2]:pp.75–79

$f^*(x^*) = \sup_{x \in X} \left \{\langle x^*,x \rangle - f(x) \right \}.$

### Biconjugate

The biconjugate of a function f : XR ∪ {±∞} is the conjugate of the conjugate, typically written as f** : XR ∪ {±∞}. The biconjugate is useful for showing when strong or weak duality hold (via the perturbation function).

For any xX the inequality f**(x) ≤ f(x) follows from the Fenchel–Young inequality. For proper functions, f = f** if and only if f is convex and lower semi-continuous by Fenchel–Moreau theorem.[2]:pp.75–79[3]

## Convex minimization

Main article: Convex optimization

A convex minimization (primal) problem is one of the form

$\inf_{x \in M} f(x)$

such that f : XR ∪ {±∞} is a convex function and MX is a convex set.

### Dual problem

In optimization theory, the duality principle states that optimization problems may be viewed from either of two perspectives, the primal problem or the dual problem.

In general given two dual pairs separated locally convex spaces (X, X*) and (Y, Y*). Then given the function f : XR ∪ {+∞}, we can define the primal problem as finding x such that

$\inf_{x \in X} f(x).$

If there are constraint conditions, these can be built into the function f by letting $f = f + I_{\mathrm{constraints}}$ where I is the indicator function. Then let F : X × YR ∪ {±∞} be a perturbation function such that F(x, 0) = f(x).[4]

The dual problem with respect to the chosen perturbation function is given by

$\sup_{y^* \in Y^*} -F^*(0,y^*)$

where F* is the convex conjugate in both variables of F.

The duality gap is the difference of the right and left hand sides of the inequality[2]:pp. 106–113[4][5]

$\sup_{y^* \in Y^*} -F^*(0,y^*) \le \inf_{x \in X} F(x,0).$

This principle is the same as weak duality. If the two sides are equal to each other, then the problem is said to satisfy strong duality.

There are many conditions for strong duality to hold such as:

#### Lagrange duality

For a convex minimization problem with inequality constraints,

minx f(x) subject to gi(x) ≤ 0 for i = 1, ..., m.

the Lagrangian dual problem is

supu infx L(x, u) subject to ui(x) ≥ 0 for i = 1, ..., m.

where the objective function L(x, u) is the Lagrange dual function defined as follows:

$L(x,u) = f(x) + \sum_{j=1}^m u_j g_j(x)$

## Notes

1. ^ a b c Rockafellar, R. Tyrrell (1997) [1970]. Convex Analysis. Princeton, NJ: Princeton University Press. ISBN 978-0-691-01586-6.
2. ^ a b c Zălinescu, Constantin (2002). Convex analysis in general vector spaces (J). River Edge, NJ: World Scientific Publishing Co., Inc. ISBN 981-238-067-1. MR 1921556.
3. ^ Borwein, Jonathan; Lewis, Adrian (2006). Convex Analysis and Nonlinear Optimization: Theory and Examples (2 ed.). Springer. pp. 76–77. ISBN 978-0-387-29570-1.
4. ^ a b Boţ, Radu Ioan; Wanka, Gert; Grad, Sorin-Mihai (2009). Duality in Vector Optimization. Springer. ISBN 978-3-642-02885-4.
5. ^ Csetnek, Ernö Robert (2010). Overcoming the failure of the classical generalized interior-point regularity conditions in convex optimization. Applications of the duality theory to enlargements of maximal monotone operators. Logos Verlag Berlin GmbH. ISBN 978-3-8325-2503-3.
6. ^ Borwein, Jonathan; Lewis, Adrian (2006). Convex Analysis and Nonlinear Optimization: Theory and Examples (2 ed.). Springer. ISBN 978-0-387-29570-1.
7. ^ Boyd, Stephen; Vandenberghe, Lieven (2004). Convex Optimization (PDF). Cambridge University Press. ISBN 978-0-521-83378-3. Retrieved October 3, 2011.

## References

• J.-B. Hiriart-Urruty; C. Lemaréchal (2001). Fundamentals of convex analysis. Berlin: Springer-Verlag. ISBN 978-3-540-42205-1.
• Singer, Ivan (1997). Abstract convex analysis. Canadian Mathematical Society series of monographs and advanced texts. New York: John Wiley & Sons, Inc. pp. xxii+491. ISBN 0-471-16015-6. MR 1461544.
• Stoer, J.; Witzgall, C. (1970). Convexity and optimization in finite dimensions 1. Berlin: Springer. ISBN 978-0-387-04835-2.

format: plain


text:
Michael Hong wrote:

> So for this cap, we have \$$\cap_X (x,x') = \hom(x',x) = \cup_X (x,x')\$$ ?

Right.

I find the arbitrary conventions in this course endlessly confusing, first because there are \$$2^n\$$ options some fairly large value of \$$n\$$ (like 10), second because there aren't completely standard choices in every case, and third because using Fong and Spivak's textbook I don't feel completely free to make the choices _I_ think are best!

For example: I don't like string diagrams going left to right; I like them going top to bottom. So when I say the 'cap'

$\cap_X \colon \textbf{1} \nrightarrow X \times X^{\text{op}}$

is drawn like this:

I'm already annoyed that the cap isn't being drawn as an actual cap \$$\cap\$$. And I'm also annoyed by the fact that this convention doesn't turn into my usual convention just by rotating the picture 90 degrees... I could explain that, but never mind.

But I can live with all this.

On a separate note, I really want the cap to go like this:

$\cap_X \colon \textbf{1} \nrightarrow X \times X^{\text{op}} \qquad (GOOD)$

and not this:

$\cap_X \colon \textbf{1} \nrightarrow X^{\text{op}} \times X \qquad (EVIL)$

because in the category of finite-dimensional real vector spaces we have a similar such thing for any object \$$V\$$:

$\cap_X \colon \mathbb{R} \to V \otimes V^\ast$

where \$$V \otimes V^*\$$ is the space of linear transformations of \$$V\$$ (or crudely speaking, 'square matrices') and \$$\cap_X\$$ sends the number 1 to the identity matrix. It's purely a convention that we think of linear transformation of \$$V\$$ as elements of \|(V \otimes V^\ast\\) rather than \$$V^\ast \otimes V\$$, but this conventions works well if we multiply a vector by a matrix on the _left_, as we usually do.

(Here I'm hinting at, but not really explaining, a deep connection between profunctors and linear algebra. We already seen it before: our formula for composing profunctors looks just like the formula for matrix multiplication! So, I want my conventions in these various subjects to match up nicely... and this choice of the cap makes it work.)

Given that we have

$\cap_X \colon \textbf{1} \nrightarrow X \times X^{\text{op}}$

it's easy to see that we must have \$$\cap_X(x,x') = \texttt{true}\$$ iff \$$x' \le x\$$, because this relation must remain true if we make \$$x \in X\$$ _bigger_, and also if we make \$$x' \in X^{\text{op}} \$$ _bigger_, which is the same as making \$$x' \in X\$$ _smaller_.

I could talk for hours about these interlocking conventions, since I've spent my life worrying about them.... but this is enough!


text:
# On 4-ordered Hamiltonian Graphs

I am trying to solve the following problem:

Let $G$ be a graph of order $n\geq 4$ such that deg $v \geq n/2$ for every vertex $v$ of $G$. Show that $G$ need not be 4-ordered Hamiltonian.

Here, a graph $G$ of order $n$ is $k$-ordered Hamiltonian for an integer $1 \le k \le n$ if for every ordered set $S={v_1,v_2,\dots,v_k}$ of $k$ vertices of $G$, there is a Hamiltonian cycle of $G$ encountering these $k$ vertices of $S$ in the order listed.

Here is my solution! Please let me know if this solution is not correct or does not reflect a general case:

Assume $G$ be the join of graphs $2\,K_{\frac{n-2}{2}}$ and $K_2$, i.e., $G = 2\, K_{\frac{n-2}{2}}\vee K_2$. Let $X$ and $Y$ be two sets of vertices with $\lvert X\rvert = \lvert Y\rvert = \frac{n-2}{2}$ and let $Z$ denote the set that contains the rest of the vertices of $G$. Clearly, every vertex $v$ of $G$ has degree deg $v \geq n/2$. Therefore, by Dirac's Theorem, $G$ is Hamiltonian.

To see that $G$ is not 4-ordered Hamiltonian, consider the sequence $v_1,\,v_2,\,v_3,\,v_4$ of distinct vertices of $G$, where $v_i \in X$ if $i$ is odd and $v_i \in Y$ if $i$ is even, for every $1\leq i\leq 4$.

Suppose, to the contrary, that $G$ is 4-ordered Hamiltonian. Then there exists a Hamiltonian cycle $C$ in $G$ that encounters the vertices $v_1,\,v_2,\,v_3,\,v_4$ in the considered order. Furthermore, since $C$ is a Hamiltonian cycle, it can be decomposed into 4 internally disjoint paths $P_1,\,P_2,\,P_3,\,P_4$ where $P_i$ is a $v_i-v_{i+1}$ path for $i=1,\,2,\,3$ and $P_4$ is a $v_4-v_1$ path. Observe that for each odd integer $j\,(1\leq j\leq 4)$, the vertex $v_j$ is in $X$ and is only adjacent to vertices in $Z$. Hence, each path $P_i\,(1\leq i\leq 4)$ must contain at least one vertex of $Z$. This implies that $\lvert Z\rvert \geq 4$, but $\lvert Z\rvert = 2$. Hence, we reach a contradiction and thus $G$ is not 4-ordered Hamiltonian.

Note that, although in this problem $k = 4$, it can be generalized to any value of $k$ such that $1\leq k\leq n$.

• It would be nice if the question included the somewhat obscure definition of a $4$-ordered Hamiltonian graph (for context). – Misha Lavrov Dec 6 '17 at 4:26
• @MishaLavrov Thank you for your comment. Here is the definition of a 4-ordered Hamiltonian graph: A Hamiltonian graph $G$ of order $n$ is $k$-ordered Hamiltonian for an integer $k$ with $1\leq k \leq n$ if for every ordered set $S = \{v_1,v_2,\cdots,v_k\}$ of $k$ vertices of $G$, there is a Hamiltonian cycle of $G$ encountering these $k$ vertices of $S$ in the order listed. – Morteza Soltani Dec 6 '17 at 4:33
• Thanks! I've moved this definition into the question, because nobody ever reads comments :) – Misha Lavrov Dec 6 '17 at 4:39
• @MishaLavrov Thanks a lot! – Morteza Soltani Dec 6 '17 at 4:54
• @MishaLavrov As promised I am sharing the solution that I have come up with right here :) – Morteza Soltani Dec 6 '17 at 7:37

To show that $G$ "need not be" $4$-ordered Hamiltonian, a single counter-example is enough.

The trouble is that when $n\ge 6$, $K_{n/2,n/2}$ is in fact $4$-ordered Hamiltonian: for any four vertices $v_1, v_2, v_3, v_4$, there is a Hamiltonian cycle containing those vertices in that order.

(In fact, $K_{3,3}$ was pointed out as an example of a $4$-ordered Hamiltonian graph in the original paper of Ng and Schultz defining them. From there, it is not hard to see that all larger $K_{n,n}$ are $4$-ordered Hamiltonian: the only case that cannot occur in $K_{3,3}$ is when all four vertices are on one side of the bipartition, and finding a Hamiltonian cycle visiting those vertices in any order is easy.)

It's technically true that $K_{2,2}$ is a counter-example: it has $n \ge 4$ and $\deg v \ge 2$ for all $v$, but there is only one cyclic order in which the vertices can be visited, because there is only one cycle. But I assume that the question did not intentionally allow this case, because it seems trivial.

(I would personally not be satisfied until I had a counter-example for arbitrarily large $n$, but the question does not ask for that.)

• Thanks for your prompt response. I now realized that $K_{n/2,n/2}$ can have all the possible combination of the set of four vertices of $G$ in the considered order. Although your counter example is nice and correct, I am trying to construct a generic Hamiltonian graph of order $n$ such that it is not 4-ordered Hamiltonian. – Morteza Soltani Dec 6 '17 at 4:53
• Try looking at graphs with a small vertex cut. – Misha Lavrov Dec 6 '17 at 5:03
• Thanks for the hint. I try to do so and If I could get it, I will share it right here :) – Morteza Soltani Dec 6 '17 at 5:36


text:
# 1.4: Symmetry and Physical Properties

Carrying out a symmetry operation on a molecule must not change any of its physical properties. It turns out that this has some interesting consequences, allowing us to predict whether or not a molecule may be chiral or polar on the basis of its point group.

## Polarity

For a molecule to have a permanent dipole moment, it must have an asymmetric charge distribution. The point group of the molecule not only determines whether the molecule may have a dipole moment, but also in which direction(s) it may point.

If a molecule has a $$C_n$$ axis with $$n > 1$$, it cannot have a dipole moment perpendicular to the axis of rotation (for example, a $$C_2$$ rotation would interchange the ends of such a dipole moment and reverse the polarity, which is not allowed – rotations with higher values of $$n$$ would also change the direction in which the dipole points). Any dipole must lie parallel to a $$C_n$$ axis.

Also, if the point group of the molecule contains any symmetry operation that would interchange the two ends of the molecule, such as a $$\sigma_h$$ mirror plane or a $$C_2$$ rotation perpendicular to the principal axis, then there cannot be a dipole moment along the axis.

The only groups compatible with a dipole moment are $$C_n$$, $$C_{nv}$$ and $$C_s$$. In molecules belonging to $$C_n$$ or $$C_{nv}$$ the dipole must lie along the axis of rotation.

## Chirality

One example of symmetry in chemistry that you will already have come across is found in the isomeric pairs of molecules called enantiomers. Enantiomers are non-superimposable mirror images of each other, and one consequence of this symmetrical relationship is that they rotate the plane of polarized light passing through them in opposite directions. Such molecules are said to be chiral,2 meaning that they cannot be superimposed on their mirror image. Formally, the symmetry element that precludes a molecule from being chiral is a rotation-reflection axis $$S_n$$. Such an axis is often implied by other symmetry elements present in a group.

For example, a point group that has $$C_n$$ and $$\sigma_h$$ as elements will also have $$S_n$$. Similarly, a center of inversion is equivalent to $$S_2$$. As a rule of thumb, a molecule definitely cannot have be chiral if it has a center of inversion or a mirror plane of any type ($$\sigma_h$$, $$\sigma_v$$ or $$\sigma_d$$), but if these symmetry elements are absent the molecule should be checked carefully for an $$S_n$$ axis before it is assumed to be chiral.

2 The word chiral has its origins in the Greek word for hand ($$\chi$$$$\epsilon$$$$\rho$$$$\iota$$, pronounced ‘cheri’ with a soft ch as in ‘loch’). A pair of hands is also a pair of non-superimposable mirror images, and you will often hear chirality referred to as ‘handedness’ for this reason.

1.4: Symmetry and Physical Properties is shared under a CC BY 4.0 license and was authored, remixed, and/or curated by Claire Vallance via source content that was edited to conform to the style and standards of the LibreTexts platform; a detailed edit history is available upon request.


text:
# Classical Analysis and ODEs (math.CA)

• Let $\phi$ be an $L^2$-normalized spherical vector in an everywhere unramified cuspidal automorphic representation of $\mathrm{PGL}_n$ over $\mathbb{Q}$ with Laplace eigenvalue $\lambda_{\phi}$. We establish explicit estimates for various quantities related with $\phi$ that are uniform in $\lambda_{\phi}$. This includes uniforms bounds for spherical Whittaker functions on $\mathrm{GL}_n(\mathbb{R})$, uniform bounds for the global sup-norm of $\phi$, and uniform bounds for the "essential support" of $\phi$, i.e. the region outside which it decays exponentially. The proofs combine analytic and arithmetic tools.
• In this paper, by using the atomic decomposition theory of Hardy space and weak Hardy space, we discuss the boundedness of parameterized Littlewood-Paley operator with variable kernel on these spaces.
• In this paper we solve a problem posed by H. Bommier-Hato, M. Engliš and E.H. Youssfi in [3] on the boundedness of the Bergman-type projections in generalized Fock spaces. It will be a consequence of two facts: a full description of the embeddings between generalized Fock-Sobolev spaces and a complete characterization of the boundedness of the above Bergman type projections between weighted $L^p$-spaces related to generalized Fock-Sobolev spaces.
• We consider Fock spaces $F^{p,\ell}_{\alpha}$ of entire functions on ${\mathbb C}$ associated to the weights $e^{-\alpha |z|^{2\ell}}$, where $\alpha>0$ and $\ell$ is a positive integer. We compute explicitly the corresponding Bergman kernel associated to $F^{2,\ell}_{\alpha}$ and, using an adequate factorization of this kernel, we characterize the boundedness and the compactness of the small Hankel operator $\mathfrak{h}^{\ell}_{b,\alpha}$ on $F^{p,\ell}_{\alpha}$. Moreover, we also determine when $\mathfrak{h}^{\ell}_{b,\alpha}$ is a Hilbert-Schmidt operator on $F^{2,\ell}_{\alpha}$.
• Dec 15 2017 math.CA arXiv:1712.05183v1
We consider variants on the classical Berz sublinearity theorem, using only DC, the Axiom of Dependent Choices, rather than AC, the Axiom of Choice which Berz used. We consider thinned versions, in which conditions are imposed on only part of the domain of the function -- results of quantifier-weakening type. There are connections with classical results on subadditivity. We close with a discussion of the extensive related literature.
• Recently, in the paper "The Schwarz alternating method in solid mechanics" by Alejandro Mota, Irina Tezaur and Coleman Alleman [Comput. Methods Appl. Mech. Engrg. 319 (2017) 1951] the authors extended the well known Schwarz alternating method from linear to finite-deformation solid mechanics. They developed and introduced four variants of the Schwarz alternating method, presented proof of geometric convergence of the method and prepared parallel implementation applied to some examples. Unfortunately, the work contains serious errors, both from the point of view of finite-deformation solid mechanics as well as mathematical elasticity.


text:
<img src="https://d5nxst8fruw4z.cloudfront.net/atrk.gif?account=iA1Pi1a8Dy00ym" style="display:none" height="1" width="1" alt="" />

# Chapter 4: Exercises

Difficulty Level: At Grade Created by: CK-12

Note: A calculator may be necessary for some of these problems.

1. What is the distance between (13)\begin{align*}(1\text{, }3)\end{align*} and (88)\begin{align*}(8\text{, }8)\end{align*}?
2. What is the length of x\begin{align*}x\end{align*}?
3. Do the numbers 9, 18, and 24 make up a Pythagorean triple?
4. What is the area of the triangle below?
5. What is the circumference of the circle below?
6. What is the distance between (58)\begin{align*}(-5\text{, }-8)\end{align*} and (12)\begin{align*}(1\text{, }2)\end{align*}?
7. Is a triangle with side lengths of 8, 14, and 15 acute, obtuse, or right?
8. A baseball diamond includes four bases—first, second, third, and home—that are all 90 feet apart. The path a baserunner takes involves right angles at each of the bases. Imagine a player at bat with a runner on first. The pitcher throws a wild pitch and the player on first base goes for the steal to second. Once the catcher (at home base) gets a hold of the ball, he decides to throw it over the pitcher's head to second base. How far does the catcher have to throw the ball to get the player out?
9. Imagine that you get to put a TV in your room. However, there is only enough space for a television that is 17 inches long and 15 inches high. You've already purchased a 20-inch television. Will it fit inside the space you have prepared? (Recall that televisions are measured diagonally.)
10. Find the area of the triangle.
11. Erin hurt her leg at her soccer game but still has to walk home. To keep her leg from feeling worse, she wants to take the shortest possible route. Looking at the two possible routes below, determine how much shorter the red route is than the blue. Each block has a length of 100 meters.
12. Find two points on the line y=2\begin{align*}y=2\end{align*} that are 10 units from (24)\begin{align*}(2\text{, }-4)\end{align*}.
13. In the figure below, the angles at B\begin{align*}B\end{align*} and D\begin{align*}D\end{align*} are 90\begin{align*}90^\circ\end{align*}. Find the distance of AC+CE\begin{align*}AC+CE\end{align*}.
14. Instead of walking along two sides of a rectangular field, Ryan walked along the diagonal. By taking this shortcut, he saved a distance equal to half the length of the long side of the field. Find the length of the long side of the field given that the length of the shorter side is 78 meters.

Chapter Outline

### Chapter Summary

Show Hide Details
Description
Difficulty Level:
Authors:
Tags:
Subjects:


text:
# Category: Differentiation Rules

## Constant Multiple Rule

The Constant Multiple Rule. If ${c}$ is a constant anf ${f{}}$ is a differentiable function then ${\left({c}{f{{\left({x}\right)}}}\right)}'={c}{\left({f{{\left({x}\right)}}}\right)}'$.

Proof. By definition ${\left({c}{f{{\left({x}\right)}}}\right)}'=\lim_{{{h}\to{0}}}\frac{{{c}{f{{\left({x}+{h}\right)}}}-{c}{f{{\left({x}\right)}}}}}{{h}}={c}\lim_{{{h}\to{0}}}\frac{{{f{{\left({x}+{h}\right)}}}-{f{{\left({x}\right)}}}}}{{h}}={c}{f{'}}{\left({x}\right)}$.

## Sum and Difference Rules

The Sum Rule. If $f$ and $g$ are both differentiable then ${\left({f{{\left({x}\right)}}}+{g{{\left({x}\right)}}}\right)}'={\left({f{{\left({x}\right)}}}\right)}'+{\left({g{{\left({x}\right)}}}\right)}'$.

## Product Rule

Product Rule. If $f$ and $g$ are both differentiable then ${\left({f{{\left({x}\right)}}}{g{{\left({x}\right)}}}\right)}'={f{{\left({x}\right)}}}{g{'}}{\left({x}\right)}+{f{'}}{\left({x}\right)}{g{{\left({x}\right)}}}$.

## Quotient Rule

Quotient Rule. If $f$ and $g$ are differentiable, it can be stated that ${\left(\frac{{{f{{\left({x}\right)}}}}}{{{g{{\left({x}\right)}}}}}\right)}'=\frac{{{f{'}}{\left({x}\right)}{g{{\left({x}\right)}}}-{f{{\left({x}\right)}}}{g{'}}{\left({x}\right)}}}{{{\left({g{{\left({x}\right)}}}\right)}}^{{2}}}$.

## Chain Rule

Now, let's see how to differentiate composite functions.

Suppose that we are given a function ${h}{\left({x}\right)}={f{{\left({g{{\left({x}\right)}}}\right)}}}$. Remembering that ${g{'}}{\left({x}\right)}$ is the rate of change of ${g{{\left({x}\right)}}}$ with respect to ${x}$ and ${f{'}}{\left({g{{\left({x}\right)}}}\right)}$ is the rate of change of ${f{}}$ with respect to ${g{{\left({x}\right)}}}$, it is reasonable to suggest that the rate of change of ${f{}}$ with respect to ${x}$ is the product of ${f{'}}{\left({g{{\left({x}\right)}}}\right)}$ and ${g{'}}{\left({x}\right)}$.

## Implicit Differentiation

The techniques we learned allow us to differentiate the functions like ${y}={\sqrt[{{3}}]{{{{x}}^{{2}}+{\sin{{\left({x}\right)}}}}}}$ or ${y}=\frac{{\tan{{\left({x}\right)}}}}{{{{e}}^{{{\sin{{\left({x}\right)}}}}}}}$, or, in general, ${y}={f{{\left({x}\right)}}}$. But what to do if we can't express ${y}$ in terms of ${x}$ or if the expression would be very complex?

## Derivative of Inverse Function

Now, let's use implicit differentiation to find derivatives of inverse functions.

Fact. Suppose that function ${y}={f{{\left({x}\right)}}}$ has unique inverse and has finite derivative ${f{'}}{\left({x}\right)}\ne{0}$ then derivative of inverse function ${y}={{f}}^{{-{1}}}{\left({x}\right)}$ is ${\left({{f}}^{{-{1}}}{\left({x}\right)}\right)}'=\frac{{1}}{{{f{'}}{\left({{f}}^{{-{1}}}{\left({x}\right)}\right)}}}$.

## Logarithmic Differentiation

The calculation of the derivatives of functions involving products, powers, or quotients can be simplified with logarithmic differentiation (because of the properties of logarithms).

Let's see first how to differentiate the functions that already have a product and/or a quotient under the logarithm.


text:
Article Contents
Article Contents

# Equilibrium locus of the flow on circular networks of cells

• We perform a geometric study of the equilibrium locus of the flow that models the diffusion process over a circular network of cells. We prove that when considering the set of all possible values of the parameters, the equilibrium locus is a smooth manifold with corners, while for a given value of the parameters, it is an embedded smooth and connected curve. For different values of the parameters, the curves are all isomorphic.

Moreover, we show how to build a homotopy between different curves obtained for different values of the parameter set. This procedure allows the efficient computation of the equilibrium point for each value of some first integral of the system. This point would have been otherwise difficult to be computed for higher dimensions. We illustrate this construction by some numerical experiments.

Eventually, we show that when considering the parameters as inputs, one can easily bring the system asymptotically to any equilibrium point in the reachable set, which we also easily characterize.

Mathematics Subject Classification: Primary: 57R99, 37C25; Secondary: 34H05.

 Citation:

• Figure 1.  The homotopy path generated with the following parameters ${\mathit{\boldsymbol{\lambda}}}_1 = (1, 1, 1)$, ${\mathit{\boldsymbol{\lambda}}}_2 = ( 1.39328599, 8.30098374, 3.98355604)$ and $s = 1$. The first equilibrium point $E_0 = (1/3, 1/3, 1/3)$ is represented by a green ball, while the final equilibrium point $E_1 = ( 0.53112814, 0.1203633, 0.34850856)$ is rendered as a red triangle. Of course all over the path the constraint $e_1 + e_2 + e_3 = s$ holds.

•  C. Ehresmann , Les connexions infinitésimales dans un espace fibré différentiable, Colloque de Topologie, Bruxelles 1950, Paris, (1951) , 29-55. D. Lazard  and  F. Rouillier , Solving parametric polynomial systems, Journal of Symbolic Computations, 42 (2007) , 636-667.  doi: 10.1016/j.jsc.2007.01.007. J. Lee, Introduction to Smooth Manifolds, 2$^{nd}$ , Springer, 2013. T. Y. Li , Numerical solution of multivariate polynomial systems by homotopy continuation methods, Acta Numerica, 6 (1997) , 399-436.  doi: 10.1017/S0962492900002749. J. Mather , Notes on topological stability, Bulletin of the American Mathematical Society, 49 (2012) , 475-506.  doi: 10.1090/S0273-0979-2012-01383-6. A. Raveh , Y. Zarai , M. Margaliot  and  T. Ruller , Ribosome flow model on a ring, IEEE/ACM Transactions on Computational Biology and Bioinformatics, 12 (2015) , 1429-1439.  doi: 10.1109/TCBB.2015.2418782.

Figures(1)

• on this site

/


text:
# Picking the most cost efficient sets

I have two 2D arrays: $$P[n][s]$$ and $$C[n][s]$$, $$s \leq n$$.

P contains sets of nodes and $$C$$ the cost of a set in $$P$$, e.g. the cost of $$P[2][2]$$ is $$C[2][2]$$ and a set $$p \in P = \{ s_0, s_1, …, s_{n-1} \}^q, q \leq n$$, e.g. $$p=\{s_0, s_3\}$$.

For every row I can pick at most one set but in the end the union of the picked sets needs to contain all nodes $$\{s_0, s_1, …, s_{n-1} \}$$.

How do I find the least expensive picks in linear time?


text:
Canadian Mathematical Society www.cms.math.ca
 location:  Publications → journals
Search results

Search: All articles in the CMB digital archive with keyword Bockstein maps

 Expand all        Collapse all Results 1 - 1 of 1

1. CMB 1999 (vol 42 pp. 274)

Dădărlat, Marius; Eilers, Søren
 The Bockstein Map is Necessary We construct two non-isomorphic nuclear, stably finite, real rank zero $C^\ast$-algebras $E$ and $E'$ for which there is an isomorphism of ordered groups $\Theta\colon \bigoplus_{n \ge 0} K_\bullet(E;\ZZ/n) \to \bigoplus_{n \ge 0} K_\bullet(E';\ZZ/n)$ which is compatible with all the coefficient transformations. The $C^\ast$-algebras $E$ and $E'$ are not isomorphic since there is no $\Theta$ as above which is also compatible with the Bockstein operations. By tensoring with Cuntz's algebra $\OO_\infty$ one obtains a pair of non-isomorphic, real rank zero, purely infinite $C^\ast$-algebras with similar properties. Keywords:$K$-theory, torsion coefficients, natural transformations, Bockstein maps, $C^\ast$-algebras, real rank zero, purely infinite, classificationCategories:46L35, 46L80, 19K14

© Canadian Mathematical Society, 2015 : https://cms.math.ca/


text:
# fundamental in probability & convergence with probability 1

• February 22nd 2010, 07:52 AM
cribby
fundamental in probability & convergence with probability 1
I am trying to understand a proof that if $\{X_n\}$ is fundamental in probability, then there exists a subsequence and a random variable $X$ such that the subsequence converges with probability 1 to $X$.

The proof begins with the construction, by indices, of a subsequence where $n_1 = 1$ and $n_{i+1}$ is the smallest index such that $n_{i+1} > n_i$ where $P(\{ \vert X_m - X_n \vert \geq 2^{-i}\}) < 2^{-i}$. This implies that $\sum_{k=1}^{\infty} P(\{\vert X_{n_{k+1}} - X_{n_k}\vert \geq 2^{-k}\}) < \sum_1^{\infty} 2^{-k}< \infty$.

The next line goes: Hence, $\sum_1^{\infty} \vert X_{n_{k+1}} - X_{n_k} \vert < \infty$ with probability 1.

**Can someone explain that step to me please?**

The proof goes on to use that last line to construct a set N of things for which the sum is infinite and then defines the limit r.v. $X$ to be 0 when things are in N, and $X_{n_1} + \sum_1^{\infty}(X_{n_{k+1}} - X_{n_k})$ when things are not in N.

I could also use a little explanation in understanding why this r.v. was so defined, because the subsequence constructed in the proof is supposed to converge with probability one to this random variable but I don't understand whats going on well enough to see it.

**Also, I've been looking at course notes from the past couple of weeks I've missed due to illness and I see a statement (without proof, though I think I can come up with one) that convergence with probability 1 to X is equivalent to the sequence being fundamental in probability. Wouldn't this trivially supercede the above proof? I mean, assuming the sequence is fundamental in probability, then this statement says that the entire sequence, which is trivially a subsequence of itself, converges with probability 1?**
• February 22nd 2010, 12:34 PM
Laurent
Quote:

Originally Posted by cribby
I am trying to understand a proof that if $\{X_n\}$ is fundamental in probability, then there exists a subsequence and a random variable $X$ such that the subsequence converges with probability 1 to $X$.

The proof begins with the construction, by indices, of a subsequence where $n_1 = 1$ and $n_{i+1}$ is the smallest index such that $n_{i+1} > n_i$ where $P(\{ \vert X_m - X_n \vert \geq 2^{-i}\}) < 2^{-i}$. This implies that $\sum_{k=1}^{\infty} P(\{\vert X_{n_{k+1}} - X_{n_k}\vert \geq 2^{-k}\}) < \sum_1^{\infty} 2^{-k}< \infty$.

The next line goes: Hence, $\sum_1^{\infty} \vert X_{n_{k+1}} - X_{n_k} \vert < \infty$ with probability 1.

**Can someone explain that step to me please?**

By Borel-Cantelli lemma, almost-surely there is $k_0\geq 1$ such that, for all $k\geq k_0$, $|X_{n_{k+1}}-X_{n_k}|\leq 2^{-k}$, hence $\sum_1^\infty |X_{n_{k+1}}-X_{n_k}|\leq \sum_{k=1}^{k_0-1}|X_{n_{k+1}}-X_{n_k}|+\sum_{k=k_0}^\infty \frac{1}{2^k}<\infty$.

Quote:

The proof goes on to use that last line to construct a set N of things for which the sum is infinite and then defines the limit r.v. $X$ to be 0 when things are in N, and $X_{n_1} + \sum_1^{\infty}(X_{n_{k+1}} - X_{n_k})$ when things are not in N.

I could also use a little explanation in understanding why this r.v. was so defined, because the subsequence constructed in the proof is supposed to converge with probability one to this random variable but I don't understand whats going on well enough to see it.
It is correct that the value of $X$ on $N^c$ is arbitrary; they choose it to be 0. It couldn't be defined as the limit of the series since it may not converge.

In order to be rigorous, it is important to define $X$ everywhere (as for any r.v.), even though only the values on N really matter.

Quote:

convergence with probability 1 to X is equivalent to the sequence being fundamental in probability.
This is wrong. Being "fundamental in probability" (a not so common notion, btw) is equivalent to converging in probability to some random variable.
• February 22nd 2010, 08:15 PM
cribby
Quote:

Originally Posted by Laurent
By Borel-Cantelli lemma, almost-surely there is $k_0\geq 1$ such that, for all $k\geq k_0$, $|X_{n_{k+1}}-X_{n_k}|\leq 2^{-k}$, hence $\sum_1^\infty |X_{n_{k+1}}-X_{n_k}|\leq \sum_{k=1}^{k_0-1}|X_{n_{k+1}}-X_{n_k}|+\sum_{k=k_0}^\infty \frac{1}{2^k}<\infty$.

Awesome--thanks!

Quote:

It is correct that the value of $X$ on $N^c$ is arbitrary; they choose it to be 0. It couldn't be defined as the limit of the series since it may not converge.

In order to be rigorous, it is important to define $X$ everywhere (as for any r.v.), even though only the values on N really matter.
I think I miscommunicated my difficulty with this part of the proof. What would help me get up to speed here is a genetic account of the nonzero portion of the limit r.v. I get that everything has to go somewhere and so we send the stuff we're really not interested in to some garbage value, but I'm not clear why the nonzero portion was defined the way it was. I guess what I'm looking for is some heuristic enlightenment--how, by what brain crevasses, would one generate this?

Quote:

This is wrong. Being "fundamental in probability" (a not so common notion, btw) is equivalent to converging in probability to some random variable.
Great. (Insert rant on math faculty who insist on making outdated/marginal concepts core course material here.)

I found another possible correction to the statement in the course notes--that "fundamental almost surely" is equivalent to convergence almost surely. (Insert rant on math faculty who after more than 2 decades of teaching still can't control the flow of a lecture or their boardwork here.)

Thanks again, I really appreciate it!!
• February 23rd 2010, 09:58 AM
Laurent
Quote:

Originally Posted by cribby
I think I miscommunicated my difficulty with this part of the proof. What would help me get up to speed here is a genetic account of the nonzero portion of the limit r.v. I get that everything has to go somewhere and so we send the stuff we're really not interested in to some garbage value, but I'm not clear why the nonzero portion was defined the way it was. I guess what I'm looking for is some heuristic enlightenment--how, by what brain crevasses, would one generate this?

Oh, I see... :-s
There is a very good reason for this definition: in wide generality, for a sequence $(a_n)_n$, we have $a_n=a_1+(a_2-a_1)+\cdots+(a_n-a_{n-1})$ ("telescoping sum": all terms but one cancel), hence

( $(a_n)_n$ converges toward $a$) iff (the series $\sum_k (a_{k+1}-a_k)$ converges and $a_1+\sum_{k=1}^\infty (a_{k+1}-a_k)=a$).

The series is just a convenient way to rewrite the limit since we can use one of the numerous convergence tests (here, the comparison test). Another way of writing the proof would be: "(....) thus almost-surely the series $\sum_k (X_{n_k}-X_{n_{k-1}})$ converges (since it converges absolutely), which is to say that almost-surely the sequence $(X_{n_k})_k$ converge (since $X_{n_k}=X_{n_1}+\sum_{i=2}^k (X_{n_i}-X_{n_{i-1}})$ for all $k$). Let us define $X$ to be the limit of this sequence when it converges, and 0 otherwise. "

Quote:

I found another possible correction to the statement in the course notes--that "fundamental almost surely" is equivalent to convergence almost surely.
That indeed would be correct since it is just another way of saying that a sequence converges if (and only if) it is Cauchy.


text:
## cit_util/src/OpenArrayTable.ig

$Id: OpenArrayTable.ig,v 1.2 2001-09-19 14:07:43 wagner Exp$

Copyright 1992 Digital Equipment Corporation. Distributed only by permission. See the file COPYRIGHT for a full description. Last modified on Thu Sep 22 11:05:54 PDT 1994 by heydon modified on Mon Nov 8 15:14:32 PST 1993 by mcjones modified on Sun Jan 19 18:07:07 PST 1992 by gnelson

Table is a generic interface defining partial maps that support update and iteration. \index{map!updatable} This version supports only open arrays as the key.

GENERIC INTERFACE OpenArrayTable(Key, Value);

Where Key.T is an open array type, Value.T is not an open array type, both Key and Value contain

      CONST Brand = <text-constant>;

and Key additionally contains

      PROCEDURE Equal(k1, k2: Key.T): BOOLEAN;
PROCEDURE Hash(k: Key.T): Word.T;
PROCEDURE Clone(k : Key.T) : REF Key.T;

Brand must be a text constant. It will be used to construct a brand for the opaque type Table.Default and any generic types instantiated with the Table interface. For a non-generic interface, we recommend choosing the name of the interface.

Equal must be an equivalence relation and Hash must respect that equivalence relation, in other words, if Equal(k1, k2), then Hash(k1)=Hash(k2).

Hash and Equal may be declared with a parameter mode of either VALUE or READONLY, but not VAR.

Clone must return a reference to an object of the same size as k. This object must not be referenced later.

IMPORT Word;

CONST
Brand = "(Table " & Key.Brand & " " & Value.Brand & ")";
DefaultBrand = "(Default " & Brand & ")";
(* A "Table.Default" is revealed to have the brand "DefaultBrand". *)

TYPE
T = OBJECT METHODS
get(READONLY k: Key.T; VAR v: Value.T): BOOLEAN;
delete(READONLY k: Key.T; VAR v: Value.T): BOOLEAN;
size(): CARDINAL;
iterate(): Iterator
END;
Iterator = OBJECT METHODS
next(VAR k: Key.T; VAR v: Value.T): BOOLEAN
END;
Default <: T OBJECT METHODS
init(sizeHint: CARDINAL := 0): Default;
END;
END OpenArrayTable.

A Table(Key, Value).T, or table, is a partial map from Key.Ts to Value.Ts. Actually, it turns out to be useful for a table to treat two different keys as if they are the same whenever they are equivalent according to some specified equivalence relation. For example, if you are creating a table with a Key.T of TEXT, you are likely to want Text.Equal as the equivalence relation.

Formally, a table tbl has the components:

      canon(tbl) a map on elements of Key.T
map(tbl)   a map from elements of Key.T to elements of Value.T

canon(tbl) represents an equivalence relation: canon(tbl)(k) is the {\em canonical representative} of all the keys that are equivalent to k. The domain of map(tbl) includes only canonical representatives, that is, elements in the range of canon(tbl). The equivalence relation underlying canon(tbl) must be time-invariant. For example, it can't depend on the values of particular references since some garbage collectors move REF values.

The methods of an object tbl of type Table.T have the following specifications:

The call tbl.get(k, v) sets v to map(tbl)(canon(tbl)(k)) and returns TRUE if canon(tbl)(k) is in dom(map(tbl)). Otherwise, it returns FALSE without changing v.

The call tbl.put(k, v) changes map(tbl)(canon(tbl)(k)) to v and returns TRUE if canon(k) is in dom(map(tbl)). Otherwise, it sets the value of map(tbl)(canon(tbl)(k)) to v, and returns FALSE.

The call tbl.delete(k, v) sets v to map(tbl)(canon(tbl)(k)), removes (canon(tbl)(k), v) from map(tbl), and returns TRUE if canon(tbl)(k) is in dom(map(tbl)). Otherwise, it returns FALSE without changing v.

The call tbl.size() returns the size of dom(map(tbl)), that is, the number of entries in tbl.

The call tbl.iterate() returns an iterator, which is an object that can be used to iterate over the key-value pairs in tbl. See the definition of the type Iterator below.

If i is the result of the call tbl.iterate(), then the call it.next(k, v) selects an entry from tbl that has not already been returned by i, sets k and v to its key and value, and returns TRUE. If no entries remain, the call returns FALSE without setting k or v. It is a checked runtime error to call next after it has returned FALSE. The client must ensure that while an iterator is in use, the parent table is not modified.

The type Default is an implementation of T using chained hashing. The methods specific to an object dflt of type Default have the following specifications:

The call dflt.init(sizeHint) returns dflt after initializing it to a table with an empty map(dflt). If sizeHint is greater than 0, init assumes that put will subsequently be called with at least sizeHint different keys; these calls on put may execute somewhat faster than if sizeHint was 0. The init method has side-effects on the table.

The call dflt.keyEqual(k1, k2) returns Key.Equal(k1, k2) and the call dflt.keyHash(k) returns Key.Hash(k). The other methods call keyEqual and keyHash whenever they need to consult the table's equivalence relation. This means a subtype of Default can determine the equivalence relation by overriding keyEqual and keyHash, providing keyEqual implements an equivalence relation and keyHash respects that relation.

For efficiency, tables and their iterators are not monitored, so a client accessing a table from multiple threads must ensure that if two operations are active concurrently, then neither of them has side effects on the same table or iterator. The T.put, T.delete, and Default.init methods are the only ones with side effects on the table. An iterator's next method has side-effects on the iterator.


text:
# Separable Differential Equations

Consider the differential equation y'=f(t,y), or (dy)/(dt)=f(t,y). If the function f(t,y) can be written as the product of the function g(t) (function that depends only on t) and the function u(y) (function that depends only on y), such a differential equation is called separable.

Let's see how it is solved.

(dy)/(dt)=g(t)u(y), or (dy)/(u(y))=g(t)dt.

Integrating both sides yields int (dy)/(u(y))=int g(t)dt +C, where C is an arbitrary constant.

Example 1. Solve (t+1)dt-3/y^4 dy=0, y(1)=3.

This equation is separable and can be rewrritten as 3/y^4 dy=(t+1)dt.

Integrating both sides yields int 3/y^4 dy=int (t+1)dt, or -1/(y^3)=(t^2)/2+t+C, where C is an arbitrary constant.

Rewriting it a bit, we obtain that y=-1/root(3)(1/2 t^2+t+C). This is the general solution. To find the particular solution, plug the initial values and find the constant C.

y(1)=3=-1/root(3)(1/2 1^2+1+C)-> 3/2+C=-1/27. So, C=-83/54. Thus, the particular solution is  y=-1/root(3)(1/2 t^2+t-83/54).

Now, let's take a look at another example.

Example 2. Solve y'=y^2t^2.

This equation is separable. We can rewrite it as (dy)/(dt)=y^2t^2, or (dy)/y^2=t^2dt.

Integrating both sides gives int (dy)/y^2=int t^2dt, or -1/y=1/3 t^3+C, where C is an arbitrary constant.

Thus, the general solution is y=-1/(1/3 t^3+C).

There are also 2 particular cases: when g(t)=1 (the differential equation doesn't contain t) or f(y)=1 (the differential equation doesn't contain y).

Let's do some more practice.

Example 3. Solve y'=e^(-y).

We can rewrite it as (dy)/(dt)=e^(-y) or e^y dy=dt.

Integrating both sides gives e^y=t+C, where C is an arbitrary constant.

So, the general solution is y=ln(t+C).

And one more final example.

Example 4. Solve y'=sin(t), y(0)=5.

We can rewrite it as (dy)/(dt)=sin(t), or dy=sin(t)dt.

Integrating both sides gives y=-cos(t)+C, where C is an arbitrary constant.

To find the particular solution, use the initial condition y(0)=5:

y(0)=5=-cos(0)+C ->C=6

So, the particular solution is y=-cos(t)+6.


text:
### changeset 324:06d11a6363cd

New LogicProg chapter
author Adam Chlipala Tue, 20 Sep 2011 14:07:21 -0400 3513d8b0531a 5e24554175de Makefile latex/cpdt.tex src/Intro.v src/LogicProg.v src/Match.v 5 files changed, 581 insertions(+), 182 deletions(-) [+]
line wrap: on
line diff
--- a/Makefile	Tue Sep 20 11:08:05 2011 -0400
+++ b/Makefile	Tue Sep 20 14:07:21 2011 -0400
@@ -1,7 +1,7 @@
MODULES_NODOC := CpdtTactics MoreSpecif DepList
MODULES_PROSE := Intro
MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
-	MoreDep DataStruct Equality Generic Universes Match Reflection \
+	MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
Large Firstorder DeBruijn Hoas Interps Extensional Intensional OpSem
MODULES_DOC   := $(MODULES_PROSE)$(MODULES_CODE)
MODULES       := $(MODULES_NODOC)$(MODULES_DOC)
--- a/latex/cpdt.tex	Tue Sep 20 11:08:05 2011 -0400
+++ b/latex/cpdt.tex	Tue Sep 20 14:07:21 2011 -0400
@@ -46,6 +46,7 @@
\include{Equality.v}
\include{Generic.v}
\include{Universes.v}
+\include{LogicProg.v}
\include{Match.v}
\include{Reflection.v}
\include{Large.v}
--- a/src/Intro.v	Tue Sep 20 11:08:05 2011 -0400
+++ b/src/Intro.v	Tue Sep 20 14:07:21 2011 -0400
@@ -237,6 +237,8 @@
\hline
Universes and Axioms & \texttt{Universes.v} \\
\hline
+Proof Search by Logic Programming & \texttt{LogicProg.v} \\
+\hline
Proof Search in Ltac & \texttt{Match.v} \\
\hline
Proof by Reflection & \texttt{Reflection.v} \\
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LogicProg.v	Tue Sep 20 14:07:21 2011 -0400
@@ -0,0 +1,576 @@
+ *
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *)
+
+(* begin hide *)
+
+Require Import List.
+
+Require Import CpdtTactics.
+
+Set Implicit Arguments.
+
+(* end hide *)
+
+(** %\part{Proof Engineering}
+
+   \chapter{Proof Search by Logic Programming}% *)
+
+(** Exciting new chapter that is missing prose for the new content!  Some content was moved from the next chapter, and it may not seem entirely to fit here yet. *)
+
+
+(** * Introducing Logic Programming *)
+
+Print plus.
+
+Inductive plusR : nat -> nat -> nat -> Prop :=
+| PlusO : forall m, plusR O m m
+| PlusS : forall n m r, plusR n m r
+  -> plusR (S n) m (S r).
+
+(* begin thide *)
+Hint Constructors plusR.
+(* end thide *)
+
+Theorem plus_plusR : forall n m,
+  plusR n m (n + m).
+(* begin thide *)
+  induction n; crush.
+Qed.
+(* end thide *)
+
+Theorem plusR_plus : forall n m r,
+  plusR n m r
+  -> r = n + m.
+(* begin thide *)
+  induction 1; crush.
+Qed.
+(* end thide *)
+
+Example four_plus_three : 4 + 3 = 7.
+(* begin thide *)
+  reflexivity.
+Qed.
+(* end thide *)
+
+Example four_plus_three' : plusR 4 3 7.
+(* begin thide *)
+  auto.
+Qed.
+(* end thide *)
+
+Example five_plus_three' : plusR 5 3 8.
+(* begin thide *)
+  auto 6.
+Restart.
+  info auto 6.
+Qed.
+(* end thide *)
+
+(* begin thide *)
+Hint Constructors ex.
+(* end thide *)
+
+Example seven_minus_three : exists x, x + 3 = 7.
+(* begin thide *)
+  eauto 6.
+Abort.
+(* end thide *)
+
+Example seven_minus_three' : exists x, plusR x 3 7.
+(* begin thide *)
+  info eauto 6.
+Qed.
+(* end thide *)
+
+Example seven_minus_four' : exists x, plusR 4 x 7.
+(* begin thide *)
+  info eauto 6.
+Qed.
+(* end thide *)
+
+(* begin thide *)
+SearchRewrite (O + _).
+
+Hint Immediate plus_O_n.
+
+Lemma plusS : forall n m r,
+  n + m = r
+  -> S n + m = S r.
+  crush.
+Qed.
+
+Hint Resolve plusS.
+(* end thide *)
+
+Example seven_minus_three : exists x, x + 3 = 7.
+(* begin thide *)
+  info eauto 6.
+Qed.
+(* end thide *)
+
+Example seven_minus_four : exists x, 4 + x = 7.
+(* begin thide *)
+  info eauto 6.
+Qed.
+(* end thide *)
+
+Example hundred_minus_hundred : exists x, 4 + x + 0 = 7.
+(* begin thide *)
+  eauto 6.
+Abort.
+(* end thide *)
+
+(* begin thide *)
+Lemma plusO : forall n m,
+  n = m
+  -> n + 0 = m.
+  crush.
+Qed.
+
+Hint Resolve plusO.
+(* end thide *)
+
+Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
+(* begin thide *)
+  info eauto 7.
+Qed.
+(* end thide *)
+
+Check eq_trans.
+
+Section slow.
+  Hint Resolve eq_trans.
+
+  Example three_minus_four_zero : exists x, 1 + x = 0.
+    Time eauto 1.
+    Time eauto 2.
+    Time eauto 3.
+    Time eauto 4.
+    Time eauto 5.
+    debug eauto 3.
+  Abort.
+End slow.
+
+(* begin thide *)
+Hint Resolve eq_trans : slow.
+(* end thide *)
+
+Example three_minus_four_zero : exists x, 1 + x = 0.
+(* begin thide *)
+  eauto.
+Abort.
+(* end thide *)
+
+Example seven_minus_three_again : exists x, x + 3 = 7.
+(* begin thide *)
+  eauto 6.
+Qed.
+(* end thide *)
+
+Example needs_trans : forall x y, 1 + x = y
+  -> y = 2
+  -> exists z, z + x = 3.
+(* begin thide *)
+  info eauto with slow.
+Qed.
+(* end thide *)
+
+
+(** * Searching for Underconstrained Values *)
+
+Print length.
+
+Example length_1_2 : length (1 :: 2 :: nil) = 2.
+  auto.
+Qed.
+
+Print length_1_2.
+
+(* begin thide *)
+Theorem length_O : forall A, length (nil (A := A)) = O.
+  crush.
+Qed.
+
+Theorem length_S : forall A (h : A) t n,
+  length t = n
+  -> length (h :: t) = S n.
+  crush.
+Qed.
+
+Hint Resolve length_O length_S.
+(* end thide *)
+
+Example length_is_2 : exists ls : list nat, length ls = 2.
+(* begin thide *)
+  eauto.
+
+  Show Proof.
+Abort.
+(* end thide *)
+
+Print Forall.
+
+Example length_is_2 : exists ls : list nat, length ls = 2
+  /\ Forall (fun n => n >= 1) ls.
+(* begin thide *)
+  eauto 9.
+Qed.
+(* end thide *)
+
+Definition sum := fold_right plus O.
+
+(* begin thide *)
+Lemma plusO' : forall n m,
+  n = m
+  -> 0 + n = m.
+  crush.
+Qed.
+
+Hint Resolve plusO'.
+
+Hint Extern 1 (sum _ = _) => simpl.
+(* end thide *)
+
+Example length_and_sum : exists ls : list nat, length ls = 2
+  /\ sum ls = O.
+(* begin thide *)
+  eauto 7.
+Qed.
+(* end thide *)
+
+Print length_and_sum.
+
+Example length_and_sum' : exists ls : list nat, length ls = 5
+  /\ sum ls = 42.
+(* begin thide *)
+  eauto 15.
+Qed.
+(* end thide *)
+
+Print length_and_sum'.
+
+Example length_and_sum'' : exists ls : list nat, length ls = 2
+  /\ sum ls = 3
+  /\ Forall (fun n => n <> 0) ls.
+(* begin thide *)
+  eauto 11.
+Qed.
+(* end thide *)
+
+Print length_and_sum''.
+
+
+(** * Synthesizing Programs *)
+
+Inductive exp : Set :=
+| Const : nat -> exp
+| Var : exp
+| Plus : exp -> exp -> exp.
+
+Inductive eval (var : nat) : exp -> nat -> Prop :=
+| EvalConst : forall n, eval var (Const n) n
+| EvalVar : eval var Var var
+| EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
+  -> eval var e2 n2
+  -> eval var (Plus e1 e2) (n1 + n2).
+
+(* begin thide *)
+Hint Constructors eval.
+(* end thide *)
+
+Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
+(* begin thide *)
+  auto.
+Qed.
+(* end thide *)
+
+Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
+(* begin thide *)
+  eauto.
+Abort.
+(* end thide *)
+
+(* begin thide *)
+Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
+  -> eval var e2 n2
+  -> n1 + n2 = n
+  -> eval var (Plus e1 e2) n.
+  crush.
+Qed.
+
+Hint Resolve EvalPlus'.
+
+Hint Extern 1 (_ = _) => abstract omega.
+(* end thide *)
+
+Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
+(* begin thide *)
+  eauto.
+Qed.
+(* end thide *)
+
+Print eval1'.
+
+Example synthesize1 : exists e, forall var, eval var e (var + 7).
+(* begin thide *)
+  eauto.
+Qed.
+(* end thide *)
+
+Print synthesize1.
+
+Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
+(* begin thide *)
+  eauto.
+Qed.
+(* end thide *)
+
+Print synthesize2.
+
+Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
+(* begin thide *)
+  eauto.
+Qed.
+(* end thide *)
+
+Print synthesize3.
+
+(* begin thide *)
+Theorem EvalConst' : forall var n m, n = m
+  -> eval var (Const n) m.
+  crush.
+Qed.
+
+Hint Resolve EvalConst'.
+
+Theorem zero_times : forall n m r,
+  r = m
+  -> r = 0 * n + m.
+  crush.
+Qed.
+
+Hint Resolve zero_times.
+
+Theorem EvalVar' : forall var n,
+  var = n
+  -> eval var Var n.
+  crush.
+Qed.
+
+Hint Resolve EvalVar'.
+
+Theorem plus_0 : forall n r,
+  r = n
+  -> r = n + 0.
+  crush.
+Qed.
+
+Theorem times_1 : forall n, n = 1 * n.
+  crush.
+Qed.
+
+Hint Resolve plus_0 times_1.
+
+Require Import Arith Ring.
+
+Theorem combine : forall x k1 k2 n1 n2,
+  (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
+  intros; ring.
+Qed.
+
+Hint Resolve combine.
+
+Theorem linear : forall e, exists k, exists n,
+  forall var, eval var e (k * var + n).
+  induction e; crush; eauto.
+Qed.
+
+Print linear.
+(* end thide *)
+
+
+(** * More on [auto] Hints *)
+
+(** Another class of built-in tactics includes [auto], [eauto], and [autorewrite].  These are based on %\textit{%##hint databases##%}%, which we have seen extended in many examples so far.  These tactics are important, because, in Ltac programming, we cannot create %%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files.  We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments.
+
+The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and [Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal.  Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db].  This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db].  An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db].  The default depth is 5.
+
+All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern].  A few examples should do best to explain how [Hint Extern] works. *)
+
+Theorem bool_neq : true <> false.
+(* begin thide *)
+  auto.
+
+  (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
+
+Abort.
+
+(** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove.  Luckily, a simpler form suffices. *)
+
+Hint Extern 1 (_ <> _) => congruence.
+
+Theorem bool_neq : true <> false.
+  auto.
+Qed.
+(* end thide *)
+
+(** Our hint says: %%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''%  The [1] is a cost for this rule.  During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints.
+
+[Extern] hints may be implemented with the full Ltac language.  This example shows a case where a hint uses a [match]. *)
+
+Section forall_and.
+  Variable A : Set.
+  Variables P Q : A -> Prop.
+
+  Hypothesis both : forall x, P x /\ Q x.
+
+  Theorem forall_and : forall z, P z.
+(* begin thide *)
+    crush.
+
+    (** [crush] makes no progress beyond what [intros] would have accomplished.  [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal.  However, we can teach [auto] to handle this kind of goal. *)
+
+    Hint Extern 1 (P ?X) =>
+      match goal with
+        | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
+      end.
+
+    auto.
+  Qed.
+(* end thide *)
+
+  (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic.  [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *)
+
+End forall_and.
+
+(** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
+
+   [[
+  Hint Extern 1 (?P ?X) =>
+    match goal with
+      | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
+    end.
+
+User error: Bound head variable
+
+   ]]
+
+   Coq's [auto] hint databases work as tables mapping %\textit{%##head symbols##%}% to lists of tactics to try.  Because of this, the constant head of an [Extern] pattern must be determinable statically.  In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
+
+   This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion.  This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in the next chapter. *)
+
+
+(** * Rewrite Hints *)
+
+   (** We have used [Hint Rewrite] in many examples so far.  [crush] uses these hints by calling [autorewrite].  Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database.  This is because, in contrast to [auto], [autorewrite] has no default database.  Thus, we set the convention that [crush] uses the [cpdt] database.
+
+   This example shows a direct use of [autorewrite]. *)
+
+Section autorewrite.
+  Variable A : Set.
+  Variable f : A -> A.
+
+  Hypothesis f_f : forall x, f (f x) = f x.
+
+  Hint Rewrite f_f : my_db.
+
+  Lemma f_f_f : forall x, f (f (f x)) = f x.
+    intros; autorewrite with my_db; reflexivity.
+  Qed.
+
+  (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints.  First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate.  Second, we may add hints that %%#"#lead [autorewrite] down the wrong path.#"#%''%  For instance: *)
+
+  Section garden_path.
+    Variable g : A -> A.
+    Hypothesis f_g : forall x, f x = g x.
+    Hint Rewrite f_g : my_db.
+
+    Lemma f_f_f' : forall x, f (f (f x)) = f x.
+      intros; autorewrite with my_db.
+      (** [[
+============================
+ g (g (g x)) = g x
+          ]]
+          *)
+
+    Abort.
+
+    (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied.  This %%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %%#"#break#"#%''% old proofs.  The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them.  The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
+
+  Reset garden_path.
+
+  (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
+
+  Section garden_path.
+    Variable P : A -> Prop.
+    Variable g : A -> A.
+    Hypothesis f_g : forall x, P x -> f x = g x.
+    Hint Rewrite f_g : my_db.
+
+    Lemma f_f_f' : forall x, f (f (f x)) = f x.
+      intros; autorewrite with my_db.
+      (** [[
+
+  ============================
+   g (g (g x)) = g x
+
+subgoal 2 is:
+ P x
+subgoal 3 is:
+ P (f x)
+subgoal 4 is:
+ P (f x)
+          ]]
+          *)
+
+    Abort.
+
+    (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
+
+  Reset garden_path.
+
+  (** Our final, successful, attempt uses an extra argument to [Hint Rewrite] that specifies a tactic to apply to generated premises.  Such a hint is only used when the tactic succeeds for all premises, possibly leaving further subgoals for some premises. *)
+
+  Section garden_path.
+    Variable P : A -> Prop.
+    Variable g : A -> A.
+    Hypothesis f_g : forall x, P x -> f x = g x.
+(* begin thide *)
+    Hint Rewrite f_g using assumption : my_db.
+(* end thide *)
+
+    Lemma f_f_f' : forall x, f (f (f x)) = f x.
+(* begin thide *)
+      intros; autorewrite with my_db; reflexivity.
+    Qed.
+(* end thide *)
+
+    (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
+
+    Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
+(* begin thide *)
+      intros; autorewrite with my_db; reflexivity.
+(* end thide *)
+    Qed.
+  End garden_path.
+
+  (** remove printing * *)
+
+  (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
+
+  (** printing * $*$ *)
+
+  Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
+    -> f x = f (f (f y)).
+(* begin thide *)
+    intros; autorewrite with my_db in *; assumption.
+(* end thide *)
+  Qed.
+
+End autorewrite.
--- a/src/Match.v	Tue Sep 20 11:08:05 2011 -0400
+++ b/src/Match.v	Tue Sep 20 14:07:21 2011 -0400
@@ -16,9 +16,7 @@
(* end hide *)

-(** %\part{Proof Engineering}
-
-   \chapter{Proof Search in Ltac}% *)
+(** %\chapter{Proof Search in Ltac}% *)

(** We have seen many examples of proof automation so far.  This chapter aims to give a principled presentation of the features of Ltac, focusing in particular on the Ltac [match] construct, which supports a novel approach to backtracking search.  First, though, we will run through some useful automation tactics that are built into Coq.  They are described in detail in the manual, so we only outline what is possible. *)

@@ -31,184 +29,6 @@
The %\textit{%##setoid##%}% facility makes it possible to register new equivalence relations to be understood by tactics like [rewrite].  For instance, [Prop] is registered as a setoid with the equivalence relation %%#"#if and only if.#"#%''%  The ability to register new setoids can be very useful in proofs of a kind common in math, where all reasoning is done after %%#"#modding out by a relation.#"#%''% *)

-(** * Hint Databases *)
-
-(** Another class of built-in tactics includes [auto], [eauto], and [autorewrite].  These are based on %\textit{%##hint databases##%}%, which we have seen extended in many examples so far.  These tactics are important, because, in Ltac programming, we cannot create %%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files.  We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments.
-
-The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructor type], which acts like [Resolve] applied to every constructor of an inductive type; and [Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal.  Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db].  This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db].  An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db].  The default depth is 5.
-
-All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern].  A few examples should do best to explain how [Hint Extern] works. *)
-
-Theorem bool_neq : true <> false.
-(* begin thide *)
-  auto.
-
-  (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
-
-Abort.
-
-(** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove.  Luckily, a simpler form suffices. *)
-
-Hint Extern 1 (_ <> _) => congruence.
-
-Theorem bool_neq : true <> false.
-  auto.
-Qed.
-(* end thide *)
-
-(** Our hint says: %%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''%  The [1] is a cost for this rule.  During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints.
-
-[Extern] hints may be implemented with the full Ltac language.  This example shows a case where a hint uses a [match]. *)
-
-Section forall_and.
-  Variable A : Set.
-  Variables P Q : A -> Prop.
-
-  Hypothesis both : forall x, P x /\ Q x.
-
-  Theorem forall_and : forall z, P z.
-(* begin thide *)
-    crush.
-
-    (** [crush] makes no progress beyond what [intros] would have accomplished.  [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal.  However, we can teach [auto] to handle this kind of goal. *)
-
-    Hint Extern 1 (P ?X) =>
-      match goal with
-        | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
-      end.
-
-    auto.
-  Qed.
-(* end thide *)
-
-  (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic.  [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *)
-
-End forall_and.
-
-(** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
-
-   [[
-  Hint Extern 1 (?P ?X) =>
-    match goal with
-      | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
-    end.
-
-User error: Bound head variable
-
-   ]]
-
-   Coq's [auto] hint databases work as tables mapping %\textit{%##head symbols##%}% to lists of tactics to try.  Because of this, the constant head of an [Extern] pattern must be determinable statically.  In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
-
-   This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion.  This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in later sections of the chapter.
-
-   We have used [Hint Rewrite] in many examples so far.  [crush] uses these hints by calling [autorewrite].  Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database.  This is because, in contrast to [auto], [autorewrite] has no default database.  Thus, we set the convention that [crush] uses the [cpdt] database.
-
-   This example shows a direct use of [autorewrite]. *)
-
-Section autorewrite.
-  Variable A : Set.
-  Variable f : A -> A.
-
-  Hypothesis f_f : forall x, f (f x) = f x.
-
-  Hint Rewrite f_f : my_db.
-
-  Lemma f_f_f : forall x, f (f (f x)) = f x.
-    intros; autorewrite with my_db; reflexivity.
-  Qed.
-
-  (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints.  First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate.  Second, we may add hints that %%#"#lead [autorewrite] down the wrong path.#"#%''%  For instance: *)
-
-  Section garden_path.
-    Variable g : A -> A.
-    Hypothesis f_g : forall x, f x = g x.
-    Hint Rewrite f_g : my_db.
-
-    Lemma f_f_f' : forall x, f (f (f x)) = f x.
-      intros; autorewrite with my_db.
-      (** [[
-============================
- g (g (g x)) = g x
-          ]]
-          *)
-
-    Abort.
-
-    (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied.  This %%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %%#"#break#"#%''% old proofs.  The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them.  The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
-
-  Reset garden_path.
-
-  (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
-
-  Section garden_path.
-    Variable P : A -> Prop.
-    Variable g : A -> A.
-    Hypothesis f_g : forall x, P x -> f x = g x.
-    Hint Rewrite f_g : my_db.
-
-    Lemma f_f_f' : forall x, f (f (f x)) = f x.
-      intros; autorewrite with my_db.
-      (** [[
-
-  ============================
-   g (g (g x)) = g x
-
-subgoal 2 is:
- P x
-subgoal 3 is:
- P (f x)
-subgoal 4 is:
- P (f x)
-          ]]
-          *)
-
-    Abort.
-
-    (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
-
-  Reset garden_path.
-
-  (** Our final, successful, attempt uses an extra argument to [Hint Rewrite] that specifies a tactic to apply to generated premises.  Such a hint is only used when the tactic succeeds for all premises, possibly leaving further subgoals for some premises. *)
-
-  Section garden_path.
-    Variable P : A -> Prop.
-    Variable g : A -> A.
-    Hypothesis f_g : forall x, P x -> f x = g x.
-(* begin thide *)
-    Hint Rewrite f_g using assumption : my_db.
-(* end thide *)
-
-    Lemma f_f_f' : forall x, f (f (f x)) = f x.
-(* begin thide *)
-      intros; autorewrite with my_db; reflexivity.
-    Qed.
-(* end thide *)
-
-    (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
-
-    Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
-(* begin thide *)
-      intros; autorewrite with my_db; reflexivity.
-(* end thide *)
-    Qed.
-  End garden_path.
-
-  (** remove printing * *)
-
-  (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
-
-  (** printing * $*$ *)
-
-  Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
-    -> f x = f (f (f y)).
-(* begin thide *)
-    intros; autorewrite with my_db in *; assumption.
-(* end thide *)
-  Qed.
-
-End autorewrite.
-
-
(** * Ltac Programming Basics *)

(** We have already seen many examples of Ltac programs.  In the rest of this chapter, we attempt to give a more principled introduction to the important features and design patterns.


text:
# Binary tree fractal

Today's challenge is to draw a binary tree as beautiful like this example:

                               /\
/  \
/    \
/      \
/        \
/          \
/            \
/              \
/                \
/                  \
/                    \
/                      \
/                        \
/                          \
/                            \
/                              \
/\                              /\
/  \                            /  \
/    \                          /    \
/      \                        /      \
/        \                      /        \
/          \                    /          \
/            \                  /            \
/              \                /              \
/\              /\              /\              /\
/  \            /  \            /  \            /  \
/    \          /    \          /    \          /    \
/      \        /      \        /      \        /      \
/\      /\      /\      /\      /\      /\      /\      /\
/  \    /  \    /  \    /  \    /  \    /  \    /  \    /  \
/\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\  /\
/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\

You will be given a positive integer as input. This input is the height of the tree. The above example has a height of six.

You may submit either a full-program or a function, and you are free to use any of our default IO methods. For example, printing the tree, returning a string with newlines, returning a 2d char array, saving the tree to a file, etc. would all be allowed.

Trailing spaces on each line are permitted.

Here are some examples of inputs and their corresponding outputs:

1:
/\

2:
/\
/\/\

3:
/\
/  \
/\  /\
/\/\/\/\

4:
/\
/  \
/    \
/      \
/\      /\
/  \    /  \
/\  /\  /\  /\
/\/\/\/\/\/\/\/\

5:
/\
/  \
/    \
/      \
/        \
/          \
/            \
/              \
/\              /\
/  \            /  \
/    \          /    \
/      \        /      \
/\      /\      /\      /\
/  \    /  \    /  \    /  \
/\  /\  /\  /\  /\  /\  /\  /\
/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\

Unfortunately, the output grows exponentially, so it's hard to show larger examples. Here is a link to the output for 8.

As usual, this is a challenge, so standard loopholes apply, and try to write the shortest program possible in whatever language you choose.

Happy golfing!

• Can there be trailing spaces to make all line the same length? – xnor Jan 6 '17 at 6:23
• @xnor Yes, that is fine. – James Jan 6 '17 at 6:25

## Python 2, 77 bytes

S=s=i=2**input()
while s:print S/s*('/'+' '*(s-i)+'\\').center(s);i-=2;s/=s/i

Prints with trailing spaces, terminating with error.

I took this code from my submission to a challenge I posed on Anarchy Golf, plus a one-byte improvement found by xsot. The hardcoded value of 128 was changed to 2**input().

The idea is that each row of the output is a segment copied one or more times. The half after the input split has one copy of each segment, the quarter after the next split has two copies, and so on, until the last line with many segments of /\.

Each segment had a / and \, with spaces in between, as well as on the outside to pad to the right length. The outer padding is done with center.

The variable s tracks the current with of each segment, and the number of segments is S/s so that the total width is the tree width S. The line number i counts down by 2's, and whenever the value s is half of it, a split occurs, and the segment width halves. This is done via the expression s/=s/i. When i reaches 0, this gives an error that terminates the program.

Since anagolf only allows program submissions, I didn't explore the possibility of a recursive function, which I think is likely shorter.

# V, 32 bytes

é\é/ÀñLyPÄlx$X>>îò^llÄlxxbPò |  Try it online! Hexdump: 00000000: e95c e92f c0ad f116 4c79 50c4 6c78 2458 .\./....LyP.lx$X
00000010: 3e3e eef2 5e6c 6cc4 6c78 7862 50f2 0a7c  >>..^ll.lxxbP..|

# Canvas, 11 bytes

/║╶╷［ｌ＼；∔↔║

Try it here!

Explanation:

/║          push /\ ("/" palindromized so this is a Canvas object)
╶╷[       repeat input-1 times
l        get the width of the ToS
\       create a diagonal that long
;∔     prepend that to the item below
↔    reverse the thing horizontally
║   and palindromize it horizontally

# Haskell, 140 138 135 bytes

e n=[1..n]>>" "
n!f=(e n++).(++e n)<$>f f 0=[] f n=1!f(n-1)++['/':e(2*n-2)++"\\"] b n|n<2=f 1|t<-b$n-1,m<-2^(n-2)=m!f m++zipWith(++)t t

Try it online! Call with b 5, returns a list of strings.

Pretty print usage:

*Main> putStr . unlines $b 5 /\ / \ / \ / \ / \ / \ / \ / \ /\ /\ / \ / \ / \ / \ / \ / \ /\ /\ /\ /\ / \ / \ / \ / \ /\ /\ /\ /\ /\ /\ /\ /\ /\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\  (some) Explanation: • e n generates a string of n spaces • n!f pads each string in the list of strings f with n spaces left and right • f n draws a "peak" in a n by 2n rectangle • b n draws the binary tree by concatenating two smaller trees and centers a new peak above them Edit: -3 bytes thanks to Zgarb! • I think 1!f(n-1) and m!f m should save a couple of bytes. – Zgarb Jan 7 '17 at 13:14 • @Zgarb Thanks for pointing out, those precedence rules sometimes get confusing. – Laikoni Jan 7 '17 at 13:44 ## J, 49 43 42 bytes ' /\'{~(|.,-)"1@(=@i.@#,-)^:(<:(,:@,&*-))  This evaluates to a verb that takes a number and returns a 2D character array. Try it online! ## Explanation I first construct a matrix of the values -1, 0 and 1 by iterating an auxiliary verb, and then replace the numbers by characters. The auxiliary verb constructs the right half of the next iteration, then mirrors it horizontally to produce the rest. In the following explanation, , concatenates 2D arrays vertically and 1D arrays horizontally. ' /\'{~(|.,-)"1@(=@i.@#,-)^:(<:(,:@,&*-)) Input is n. ^:( ) Iterate this verb <: n-1 times ( ) starting from ,&*- the array 1 -1 (actually sign(n), sign(-n)) ,:@ shaped into a 1x2 matrix: Previous iteration is y. # Take height of y, i.@ turn into range =@ and form array of self-equality. This results in the identity matrix with same height as y. ,- Concatenate with -y, pad with 0s. ( )"1@( ) Then do to every row: |.,- Concatenate reversal to negation. ' /\'{~ Finally index entry-wise into string.  # Charcoal, 12 bytes ＦＮ«→↗⌈Ｘ²⊖ι‖Ｍ  Try it online! Link is to verbose version of code. Explanation:  Ｎ Input as a number Ｆ « Loop over implicit range → Move right (because mirroring moves the cursor) ι Current index ⊖ Decremented Ｘ² Power of 2 ⌈ Ceiling ↗ Draw diagonal line ‖Ｍ Mirror image  The line lengths are 1, 1, 2, 4, 8 ... 2^(N-2), thus the awkward calculation. # Stax, 20 19 bytes ≡mX░R○k╣∙╒ab^◘⌐╖x▼;  Run and debug it ## JavaScript (ES6), 105 bytes f=n=>n<2?"/\\":" "+f(n-1).split/[0].replace(/|/g,"$$'$'/$$\\$'$'$ \n")+f(n-1).replace(/.*/g,"$&$&")  Works by building the result up recursively from the base case /\. The bottom half is just the previous case with each line duplicated. The top half was a little trickier; it looks as if you want to take the previous case and only keep the two sides but you also have to worry about padding the strings to double the width, so instead I do some regex magic. By taking the leading spaces from the previous case and splitting at every point, I can consider the spaces before and after that point. At each match the spaces before increase by 1 and the spaces after decrease by 1; this can be used to position the / and \ in the correct places. The newlines and padding are also added here; this takes care of all the padding except a trailing space on each line and a leading space on the first line which I have to add manually. (Leading spaces on subsequent lines come from the matched string). ## Batch, 218 bytes @echo off set/a"n=1<<%1" set s=set t= %s%/\ set l=for /l %%i in (2,1,%n%)do call %l% %s% %%t%% %l%:l :l echo %t% set/an-=1,m=n^&n-1 %s%%t: /=/ % %s%%t:\ = \% if %m% neq 0 exit/b %s%%t:/ =/\% %s%%t: \=/\%  Note: Line 6 ends in a space. Works by moving the branches left and right appropriately each time, except on rows that are 2n from the end, in which case the branches get forked instead. # Haxe, 181 bytes function g(n):String return(n-=2)==-1?"/\\":[for(y in 0...1<<n)[for(x in 0...4<<n)x+y+1==2<<n?"/":x-y==2<<n?"\\":" "].join("")].concat([for(y in g(n+1).split("\n"))y+y]).join("\n");  Or, with some optional whitespace: function g(n):String return (n -= 2) == -1 ? "/\\" : [ for (y in 0...1 << n) [ for (x in 0...4 << n) x + y + 1 == 2 << n ? "/" : x - y == 2 << n ? "\\" : " " ].join("") ].concat([ for (y in g(n + 1).split("\n")) y + y ]).join("\n");  I was working for a while on a solution which created an array of space characters of the right size first, then iteratively put the forked paths lower and lower (and more densely at each iteration). It remained 230+ bytes, though. The approach here is pretty much what @Laikoni's Haskell approach is. I couldn't get away with not having :String, because Haxe is not smart enough to identify that the return type will always be a String. This is a function only, here's a full programme to test it: class Main { public static function main(){ function g(n):String return(n-=2)==-1?"/\\":[for(y in 0...1<<n)[for(x in 0...4<<n)x+y+1==2<<n?"/":x-y==2<<n?"\\":" "].join("")].concat([for(y in g(n+1).split("\n"))y+y]).join("\n"); Sys.println(g(Std.parseInt(Sys.args()[0]))); } }  Put the above in Main.hx, compile with haxe -main Main.hx -neko frac.n and test with neko frac.n 4 (replace 4 with the desired order). # PHP, 188 Bytes Online Version function f($l,$r=0,$m=1){global$a;for(;$i<$l;$i++)$i<$l/2?$a[$i+$r]=str_repeat(str_pad("/".str_pad("",2*$i)."\\",2*$l," ",2),$m):f($l/2^0,$r+$l/2,2*$m);}f(2**$argv[1]/2);echo join("\n",$a);

Expanded

function f($l,$r=0,$m=1){ global$a;
for(;$i<$l;$i++)$i<$l/2 ?$a[$i+$r]=str_repeat(str_pad("/".str_pad("",2*$i)."\\",2*$l," ",2),$m) :f($l/2^0,$r+$l/2,2*$m); } f(2**$argv[1]/2);
echo join("\n",\$a);
`


text:
, 18.10.2019 10:30, sammyraegarrett

# Use 1,2,3,4,5 to make a multiplication problem with the greatest product

### Other questions on the subject: Mathematics

Mathematics, 21.06.2019 12:30, khynia11
Eric drew a scale drawing of a country park. the scale he used was 1 inch = 2.5 yards. the picnic area is 80 yards wide in real life. how wide is the picnic area in the drawing ?
Is fgh ~ jkl? if so, identify the similarity postulate or theorem that applies.
Mathematics, 21.06.2019 18:20, holmesleauja
Type the correct answer in each box. use numerals instead of words. if necessary, use / for the fraction bar. consider the given table.
Mathematics, 21.06.2019 21:00, ShahinF7536
Graph the equationy=x^2 -$$y = x^{2} - 2$$
Do you know the correct answer?
Use 1,2,3,4,5 to make a multiplication problem with the greatest product...

### Questions in other subjects:

Mathematics, 14.04.2020 21:22
Social Studies, 14.04.2020 21:22
Total solved problems on the site: 8853690


text:
# Search for Low Mass Exotic mesonic structures. Part II: attempts to understand the experimental results

Abstract : Our previous paper, part I of the same study, shows the different experimental spectra used to conclude on the genuine existence of narrow, weakly excited mesonic structures, having masses below and a little above the pion (M=139.56 MeV) mass. This work \cite{previous} was instigated by the observation, in the $\Sigma^{+}$ disintegration: $\Sigma^{+}\to$pP$^{0}$, P$^{0}\to\mu^{-}\mu^{+}$ \cite{park}, of a narrow range of dimuon masses. The authors conclude on the existence of a neutral intermediate state P$_{0}$, with a mass M=214.3 MeV $\pm$ 0.5 MeV. We present here some attempts to understand the possible nature of the structures observed in part I.
Document type :
Journal articles

http://hal.in2p3.fr/in2p3-00179299
Contributor : Suzanne Robert <>
Submitted on : Monday, October 15, 2007 - 11:35:51 AM
Last modification on : Wednesday, September 16, 2020 - 4:08:24 PM

### Citation

B. Tatischeff, E. Tomasi-Gustafsson. Search for Low Mass Exotic mesonic structures. Part II: attempts to understand the experimental results. Physics of Particles and Nuclei Letters / PisВ'ma v Zhurnal Fizika Elementarnykh Chastits i Atomnogo Yadra, MAIK Nauka/Interperiodica, 2008, 8, pp.420-422. ⟨10.1134/S1547477108050026⟩. ⟨in2p3-00179299⟩

Record views


text:
# vertexCoverNumber -- returns the vertex cover number of a graph

## Synopsis

• Usage:
v = vertexCoverNumber G
• Inputs:
• G, an instance of the type Graph,
• Outputs:
• v, an integer, the vertex cover number of graph G

## Description

The vertex cover number is the minimum length of the set of vertex covers of a graph.

 i1 : G = graph({{1,2},{1,3},{1,4},{2,3}},EntryMode=>"edges"); i2 : vertexCoverNumber G o2 = 2


text:
Finance - Maple Help

Home : Support : Online Help : Mathematics : Finance : Cash Flow Analysis : Finance/AccruedAmount

Finance

 AccruedAmount
 calculate the accrued amount of a bond

 Calling Sequence AccruedAmount(bond, date)

Parameters

 bond - fixed- or floating-rate bond data structure; bond date - a string containing a date specification in a format recognized by ParseDate or a date data structure; evaluation date

Description

 • The AccruedAmount command computes the interest that is due on a bond since the last interest payment was made. Accrued interest is added to the contract price of a bond transaction.
 • The parameter bond is a fixed coupon bond or floating rate bond.
 • The (optional) parameter date is the evaluation date. By default the global evaluation date is used. It can be specified in any of the standard date formats supported by the package.
 • Note that the value returned by the AccruedAmount command depends on the day count and day rolling conventions used by bond.

Examples

 > $\mathrm{with}\left(\mathrm{Finance}\right):$
 > $\mathrm{SetEvaluationDate}\left("March 15, 2005"\right):$
 > $\mathrm{EvaluationDate}\left(\right)$
 ${"March 15, 2005"}$ (1)
 > $\mathrm{Settings}\left(\left[\mathrm{compounding}=\mathrm{Continuous},\mathrm{settlementdays}=0,\mathrm{businessdayconvention}=\mathrm{Unadjusted}\right]\right)$
 $\left[{\mathrm{compounding}}{=}{\mathrm{Continuous}}{,}{\mathrm{settlementdays}}{=}{0}{,}{\mathrm{businessdayconvention}}{=}{\mathrm{Unadjusted}}\right]$ (2)

Consider a 3-year bond with face value of 100 that pays a fixed coupon of 3 percent issued on March 15, 2005.

 > $\mathrm{Principal}≔100:$
 > $\mathrm{Coupon}≔0.03:$
 > $\mathrm{B1}≔\mathrm{FixedCouponBond}\left(\mathrm{Principal},3,\mathrm{Years},\mathrm{Coupon},\mathrm{issuedate}="March 15, 2005",\mathrm{daycounter}=\mathrm{Thirty360European}\right):$

Here is the same bond but using the ISDA convention.

 > $\mathrm{B2}≔\mathrm{FixedCouponBond}\left(\mathrm{Principal},3,\mathrm{Years},\mathrm{Coupon},\mathrm{issuedate}="March 15, 2005",\mathrm{daycounter}=\mathrm{ISDA}\right):$

Here is the interest accrued before the first coupon payment.

 > $\mathrm{AccruedAmount}\left(\mathrm{B1},"March 14, 2006"\right)$
 ${2.991666667}$ (3)
 > $\mathrm{AccruedAmount}\left(\mathrm{B2},"March 14, 2006"\right)$
 ${2.991780822}$ (4)

Compare this to

 > $\mathrm{Principal}\mathrm{Coupon}\mathrm{YearFraction}\left("March 15, 2005","March 14, 2006",\mathrm{Thirty360European}\right)$
 ${2.991666667}$ (5)
 > $\mathrm{Principal}\mathrm{Coupon}\mathrm{YearFraction}\left("March 15, 2005","March 14, 2006",\mathrm{ISDA}\right)$
 ${2.991780822}$ (6)

This shows the interest accrued right after the first coupon payment.

 > $\mathrm{AccruedAmount}\left(\mathrm{B1},"March 15, 2006"\right)$
 ${0.}$ (7)
 > $\mathrm{AccruedAmount}\left(\mathrm{B2},"March 15, 2006"\right)$
 ${0.}$ (8)

Here is the interest accrued two months after the first coupon payment.

 > $\mathrm{AccruedAmount}\left(\mathrm{B1},"May 16, 2006"\right)$
 ${0.5083333333}$ (9)
 > $\mathrm{AccruedAmount}\left(\mathrm{B2},"May 16, 2006"\right)$
 ${0.5095890411}$ (10)

Compare accrued interest and the difference between the clean price and the dirty price of a bond.

 > $\mathrm{SetEvaluationDate}\left("March 14, 2006"\right):$
 > $\mathrm{EvaluationDate}\left(\right)$
 ${"March 14, 2006"}$ (11)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)$
 ${96.04651941}$ (12)
 > $\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${99.03818607}$ (13)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B1}\right)=\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${99.03818608}{=}{99.03818607}$ (14)
 > $\mathrm{CleanPrice}\left(\mathrm{B2},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B2}\right)=\mathrm{DirtyPrice}\left(\mathrm{B2},0.05\right)$
 ${99.03412275}{=}{99.03412275}$ (15)
 > $\mathrm{SetEvaluationDate}\left("March 15, 2006"\right):$
 > $\mathrm{EvaluationDate}\left(\right)$
 ${"March 15, 2006"}$ (16)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)$
 ${96.05194233}$ (17)
 > $\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${96.05194233}$ (18)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B1}\right)=\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${96.05194233}{=}{96.05194233}$ (19)
 > $\mathrm{CleanPrice}\left(\mathrm{B2},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B2}\right)=\mathrm{DirtyPrice}\left(\mathrm{B2},0.05\right)$
 ${96.04769000}{=}{96.04769000}$ (20)
 > $\mathrm{SetEvaluationDate}\left("March 16, 2006"\right):$
 > $\mathrm{EvaluationDate}\left(\right)$
 ${"March 16, 2006"}$ (21)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)$
 ${96.05695047}$ (22)
 > $\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${96.06528381}$ (23)
 > $\mathrm{CleanPrice}\left(\mathrm{B1},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B1}\right)=\mathrm{DirtyPrice}\left(\mathrm{B1},0.05\right)$
 ${96.06528380}{=}{96.06528381}$ (24)
 > $\mathrm{CleanPrice}\left(\mathrm{B2},0.05\right)+\mathrm{AccruedAmount}\left(\mathrm{B2}\right)=\mathrm{DirtyPrice}\left(\mathrm{B2},0.05\right)$
 ${96.06084812}{=}{96.06084812}$ (25)

Compatibility

 • The Finance[AccruedAmount] command was introduced in Maple 15.


text:
It is currently 22 Jul 2019, 18:35

### GMAT Club Daily Prep

#### Thank you for using the timer - this advanced tool can estimate your performance and suggest more practice questions. We have subscribed you to Daily Prep Questions via email.

Customized
for You

we will pick new questions that match your level based on your Timer History

Track

every week, we’ll send you an estimated GMAT score based on your performance

Practice
Pays

we will pick new questions that match your level based on your Timer History

# If b/a+b

Author Message
TAGS:
Founder
Joined: 18 Apr 2015
Posts: 7426
Followers: 126

Kudos [?]: 1457 [0], given: 6628

If b/a+b [#permalink]  08 Jan 2018, 14:27
Expert's post
00:00

Question Stats:

85% (00:35) correct 14% (00:40) wrong based on 28 sessions
If $$\frac{b}{a+b} = \frac{7}{12}$$, then what does $$\frac{a}{b}$$ equal ?

A. $$\frac{7}{19}$$

B. $$\frac{5}{12}$$

C. $$\frac{5}{7}$$

D. $$\frac{7}{5}$$

E. $$\frac{19}{12}$$
[Reveal] Spoiler: OA

_________________
Manager
Joined: 25 Nov 2017
Posts: 51
Followers: 0

Kudos [?]: 44 [1] , given: 5

Re: If b/a+b [#permalink]  10 Jan 2018, 01:21
1
KUDOS
Lets develop
7(a+b) = 12 b
7 a + 7b = 12b
7a = 5b
7a/b = 5
A/b = 5/7

GRE Instructor
Joined: 10 Apr 2015
Posts: 2177
Followers: 65

Kudos [?]: 1994 [1] , given: 20

Re: If b/a+b [#permalink]  10 Jan 2018, 10:47
1
KUDOS
Expert's post
Carcass wrote:
If $$\frac{b}{a+b} = \frac{7}{12}$$, then what does $$\frac{a}{b}$$ equal ?

A. $$\frac{7}{19}$$

B. $$\frac{5}{12}$$

C. $$\frac{5}{7}$$

D. $$\frac{7}{5}$$

E. $$\frac{19}{12}$$

Here's another approach that uses a often-tested property: (x + y)/z = x/z + y/z

If b/(a+b) = 7/12, then we can also say that (a + b)/b = 12/7

Applying the above property, we can write: a/b + b/b = 12/7
Simplify: a/b + 1 = 12/7
Subtract 1 from both sides to get: a/b = 12/7 - 1
Rewrite 1 as follows: a/b = 12/7 - 7/7
Evaluate: a/b = 5/7

RELATED VIDEO FROM OUR COURSE

_________________

Brent Hanneson – Creator of greenlighttestprep.com

Manager
Joined: 02 Jan 2018
Posts: 66
Followers: 0

Kudos [?]: 32 [0], given: 0

Re: If b/a+b [#permalink]  11 Jan 2018, 05:51
Re: If b/a+b   [#permalink] 11 Jan 2018, 05:51
Display posts from previous: Sort by