text:
# Dimensions and Haskell: Singletons in Action

Friday, July 19th, 2019

#### Intro

In our previous blogpost, we introduced a reader to our subject matter and briefly observed several numeric libraries in Haskell. We explained why we don’t use one of the popular libraries called GHC.TypeLits with non-inductively defined kind of type-level natural numbers. In our approach, we put dimensions of data types on the type level to avoid a large set of errors that might arise at the runtime stage. During the compile stage, one may check some properties of matrix dimensions expressed via type-level natural numbers and find out the reason of that error as a type error.

In this part, we describe our approach to the matrix data type that is parameterised via its numbers of columns and rows.

#### Foreword

We had a task to implement a few machine learning algorithms for dimensionality reduction. One important goal was to find out whether Haskell fits for such sort of tasks and make an open-source library for dimensionality reduction.

At first, we took a look at the Accelerate library due to its efficiency in parallel computations, especially using GPU. We found out that a few required functions from linear algebra were not implemented in it. By the way, we are going to implement these functions later via bindings to CUDA-solver. However, we decided to switch to REPA as a base matrix library because it contains the desired functionality.

During the implementation of the given algorithms we encountered “debugging hell”, a condition, when it wasn’t possible to define the place of a mistake even if you had the place of an error. (Especially in case of PPCA which can handle and restore missed data in the input.) That’s what we had:

GPLVMHaskell-exe: inconsistent dimensions in matrix product (11,2) x (3,1)
CallStack (from HasCallStack):
error, called at src/Internal/LAPACK.hs:61:31 in
hmatrix-0.19.0.0-GJ4OJPujscCE7zmZ8JSwjL:Internal.LAPACK

Where is the place of the exception? Why such specific dimensions are there? It is a real detective job, honestly. Each time we dealt with such errors, we launched an inquiry. It was quite monotonous and exhausting. We wanted to make debugging easier and decided to lift dimensions on the type level.

Why type-level dimensions?

1. A lot of errors affect interim array dimensions.
2. We have information on unsatisfied general conditions rather than some specific numbers of dimensions that depend on the input data in the case of type errors.
3. A chance of runtime error appearance is very low on every acceptable input data – at least of error which influenсes the dimensions.

So, we decided to test this approach.

#### The Definition of Matrix

As we have said before, one needs to check matrix dimensions and their properties at the type level. For this purpose, we promoted dimensionality into the type of matrix.

DimMatrix is a newtype on Matrix r a. Note that dimensional type parameters are only on the left side of this definition.

newtype DimMatrix r (y :: Nat) (x :: Nat) a = DimMatrix { getInternal :: Matrix r a }

Here a is a type of elements, r is a representation type. y and x are types of kind Nat from type-natural library, which is the most useful for our goals, as we discussed in the introduction.

Looks good, but the dimensionality of the input data is unknown at compile-time. Thus, types might be dependent on other values received at the runtime stage. This connection might be described quite straightforwardly via dependent types. Here’s a small example written in Agda:

generateVec : {A : Set} → (ℕ → A) → (n : ℕ) → Vec A n
generateVec f zero = []
generateVec f (suc n) = (f $suc n) ∷ generateVec f n  In this example, we generate a list with length in its type, the result of which is parametrised by value n. In other words, it depends on the value. Here, the benefit of dependent types is that the compiler checks the function body. If the length of that list doesn’t equal n or the compiler cannot prove this fact, then we obtain a compilation error. At present, Haskell lacks dependent types. However, there is the necessity to jump from values to types, and we’re not able to do it with the actual Haskell type system. In singletons, one may emulate a dependent type by jump mapping some type a into a datatype Sing n, which has exactly one value in runtime. Read this article to learn more about this tool. The basic module called Singletons.Prelude provides singleton types, prelude-like type-level functions, and promoted types. The main goal of the module is to emulate Haskell prelude at the type-level. More information about promoted types you can find here. This library is pretty helpful for dependent types emulating in Haskell, but it might become irrelevant when full-fledged dependent types would be available in Haskell. This tutorial introduces singletons more systematically. We only discuss some basic constructions that we have used for type-safe dimensions. We decided to use the singletons interface for type-level dimensions. Here we meet an additional important characteristic of type-natural. There is integration between type-natural and singletons implemented as follows. Let us consider the following example of singletons use with DimMatrix data type. withMat is a function that creates the same matrix with type-level dimensions from the input repa matrix. We implemented this function via continuation-passing style because type-level dimensions x and y are bound by the internal universal quantifier so that they cannot appear in the result type k. Here, we use a continuation-passing style to create a matrix with type-level dimensionality from the usual one and avoid the disappearance of dimension in types. This function is one of the most widely used by us: withMat :: Matrix D Double -> (forall (x :: Nat) (y :: Nat). (SingI y, SingI x) => DimMatrix D x y Double -> k) -> k withMat m f = let (Z :. y :. x) = extent m in case toSing (intToNat y) of SomeSing (sy :: Sing m) -> withSingI sy$
case toSing (intToNat x) of
SomeSing (sx :: Sing n) -> withSingI sx $f (DimMatrix @D @m @n m)  #### Property Checking At the early stages, we created proofs via the function called unsafeCoerce, if some desired condition holds. After that, we used the Evidence data type that came from dimensions, where, however, type-level proofs are created via the same unsafeCoerce. Here is a simple example from the library: sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs)) sameDims as bs | listDims as == listDims bs = Just (unsafeCoerce# (E @('[] ~ '[]))) | otherwise = Nothing  In addition to type-safe dimensions itself, we also need to check their properties. For example, we need to make sure that the number of columns is less or equal to the input number. We have already promoted our dimensionality into the type level, but we also should verify their properties at the type level. Let’s look at a simple example. ... case (sing :: Sing desired) %<= (sing :: Sing x) of Proved LEQ -> foo @desired @x Disproved _ -> error "Something went wrong" ... foo :: forall (d :: Nat) (x :: Nat). (d <= x ~ 'True) => ...  where desired and x are types of the kind Nat, unknown at compile-time; foo is an arbitrary function. Here, LEQ is a constructor of the data type (:<=:) that we introduce below. This constructor stores a proof that the first argument is less or equal to the second one. Here, @ came from the language extension called TypeApplications. This extension allows us to apply functions to types as arguments explicitly. The example above is quite close to real code. We don’t know any specific dimensions at compile-time; validation of the property occurs at runtime. We ensure type system that the property holds and in the case of success, we can use it and satisfy the constraint of the function called foo. After that, we use this property in foo and other functions which will be called in foo. (:<=:) is a data type implemented as GADT that keeps a justification that$a \leq b$: data (a :: k) :<=: (b :: k) where LEQ :: forall k (a :: k) (b :: k). ((a <= b) ~ 'True) => a :<=: b  In other words, it can’t be even constructed if a > b. And the very fact of its existence proves the property. It is similar to the method of the type class SDecide called %~ type from singletons which creates a proof of propositional type equality. Similarly, (%<=) is a method of the kind class LEQDecide that we’ve introduced: class LEQDecide k where (%<=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :<=: b) infix 4 %<=  It compares two values of the Sing x type at runtime and yields a value of the type Decision (a :<=: b). Let us describe the Decision data type. In some cases, one may prove decidability of certain relations and predicates. In logic, a proposition$P$is decidable if either$P$is provable or$\not P$. In other words, we have a way to tell “Yes” or “No” based on what exactly is provable: the statement or its negation. In Haskell, the Decision data type expresses the decidability of the proposition. This type consists of the following two constructors. The first one is called Proved. This constructor stores the term that proves the desired statement. The other constructor Disproved contains a proof of negation, that is, a function a -> Void, so far as an empty type is an absurd constant logically. #### Type-safe Matrix Operations Let’s look at some examples of matrix operations that we implemented via our dimensional matrix data type. In these examples, functions mulM and transposeM are exactly sequential matrix product and transpose functions from repa-linear-functions carried through our DimMatrix data type. It’s not so difficult, really: mulM :: forall y1 x1 y2 x2 r. (x1 ~ y2) => DimMatrix r y1 x1 Double -> DimMatrix r y2 x2 Double -> DimMatrix r y1 x2 Double mulM (DimMatrix m1) (DimMatrix m2) = DimMatrix$ m1 mulS m2

transposeM :: DimMatrix r y x Double -> DimMatrix r x y Double
transposeM (DimMatrix m) = DimMatrix $transpose m  ##### Principal Component Analysis PPCA is one of the simplest procedures of dimensionality reduction. PCA is a widely used technique in pattern recognition and data compression. The process of principal components computation reduces to the finding eigenvectors and eigenvalues of the given covariance matrix. A covariance matrix is a degree of a spread of data in the given observation set. An eigenvector is a non-zero vector such that an application of the given linear operator yields the same vector up to a scalar factor, i. e. eigenvalue. You may read the more detailed description of PCA and its extensions here. Also, there is quite informative visualisation of this procedure. PCA works as follows. Suppose we have some data set, which defines as a two-dimensional matrix$M \in \mathbb{R}^{n \times m}$of real numbers and each row represents a single observation. At the next step, we need to subtract the mean from our data set for each dimension to obtain a new equivalent data set, which mean equals to zero. After that, we compute the covariance matrix, eigenvectors and eigenvalues to form the set of feature vectors. There is a statement that eigenvectors of covariance matrix form a new basis in the observed space. Eigenvector with the largest eigenvalue forms the axe with the highest dispersion along with it and the lower eigenvalue, the lower dispersions along with the corresponding axe. We can drop eigenvectors with the lowest eigenvalues and reduce the dimension with fewer information losses. Finally, the reduced principal component matrix is the product of a feature vector matrix and a transposed mean-adjusted data set that we have already obtained on the previous step. Note that the number of intended principal components is passed as a separate parameter. Now, we take a look at our PCA implementation in Haskell. We define PCA as a record data type as follows: data PCA = PCA { _inputData :: Matrix D Double , _covariance :: Matrix D Double , _eigenVectors :: Matrix D Double , _eigenValues :: Matrix D Double , _finalData :: Matrix D Double , _restoredData :: Matrix D Double , _meanMatrix :: Matrix D Double }  Names of these fields correspond to their roles: _inputData is an input matrix, etc. The type-safe version of PCA data type is implemented via DimMatrix data type, which we have already introduced above. data TypeSafePCA = forall x y d. (d <= x ~ 'True) => TypeSafePCA { desiredDim :: Proxy d , inputData_ :: DimMatrix D y x Double , covariance_ :: DimMatrix D x x Double , eigenVectors_ :: DimMatrix D x x Double , eigenValues_ :: DimMatrix D x One Double , finalData_ :: DimMatrix D y d Double , restoredData_ :: DimMatrix D y x Double , meanMatrix_ :: DimMatrix D y x Double }  In this data type, we have existentially quantified dimensions, where y is a number of columns, x is a number of rows, d is a required number of rows for the final data in an output matrix. Also, we pass a justification that$d \leq x$as the coercion constraint d <= x ~ 'True between type-level less or equal predicate and Boolean value True promoted via DataKinds. Now we have the following set of function that makes PCA from an input matrix: makePCA :: Int -> Matrix D Double -> PCA makePCA dim input = case toSing (intToNat dim) of SomeSing (sd :: Sing desired) -> withSingI sd$ withMat input $\\(inputMatrix :: DimMatrix D y x Double) -> case checkInput (Proxy @desired) (Proxy @x) of Proved LEQ -> convertTypSafeToPCA$ makePCATypeSafe (Proxy @desired) inputMatrix
Disproved _ -> error "Error: desired dimension is greater than an old number of rows"

The makePCA function takes a new number of dimensions and matrix of real numbers as arguments and yields PCA record. In this function, we promote our required dimension using the functions called toSing and intToNat, where toSing is a method SingKind kind class. intToNat is a map between integers and natural numbers defined quite naturally. The result of this embedding is a value of type SomeSing (Sing desired), where desired is our integer argument obtained after this sophisticated promotion and SomeSing is a container for a singleton unknown at compile-time.

checkInput is a function that yields the decision of $d \leq x$, where d and x are proxy arguments. Note that these type-level naturals should have instances of the SingI type class. It ensures that our type has a corresponding singleton type.

checkInput
:: forall (d :: Nat) (x :: Nat). (SingI d, SingI x)
=> Proxy d -> Proxy x -> Decision (d :<=: x)

The main logic is implemented in the function called makePCATypeSafe according to the informal description above.

makePCATypeSafe
:: forall d x y. (AllConstrained SingI '[d,x,y], d <= x ~ 'True)
=> Proxy (d :: Nat) -> DimMatrix D y x Double -> TypeSafePCA

where AllConstrained is a type family from vinyl that applies the given constraint to the type-level list.

##### Probabilistic Principal Component Analysis

In contrast to PCA, which is completely linear algebraic, probabilistic principal component analysis, or PPCA, is a probabilistic version of PCA. PPCA is a probabilistic extension of PCA. This technique defines principal axes of a matrix via maximum-likelihood estimation applying well-known expectation-maximization algorithm (or, EM-algorithm). We have two versions of PPCA. The first one is PPCA with so-called missed data. The second one lacks it.

Informally, PPCA works as follows. Let ${ x_i }, {i \in { 1, \dots, m}}$ be a data set, where $x_i \in \mathbb{R}^n$ and one needs to find a way to represent these data points as ${ z_i }, {i \in { 1, \dots, m}}$, where $z_i \in \mathbb{R}^{d}$ and $d < n$. The statement of the problem tells us that we need to optimise our data set somehow. That’s the same dimensionality reduction task, but, as you know, the devil is in the detail. In the case of PPCA, we work with the following linear model:

$z = W x + \mu + \varepsilon$

where $W \in \mathbb{R}^{d \times n}$ is a linear transformation matrix; $\varepsilon$ is Gaussian noise; $\mu$ is a mean. One should reach the estimation of the linear transformation matrix $W$ maximal likelihood. There is a way to obtain this estimation straightforwardly, but it’s very inefficiently.

And here comes the EM-algorithm. It is an iterative algorithm that consists of the following steps:

1. The initialisation of ${\bf W}$ and $\sigma^2$ by random values, where ${\bf W}$ is a linear transformation matrix from the definition above and $\sigma^2$ is a variance (in other words, squared expectation).
2. After that, we obtain the set of latent variables ${\bf Z} = {\bf z}_n$ from the corresponding a posteriori distribution of conditional probability $p({\bf z}| {\bf x})$.
3. Let us assume that ${\bf z}_n$ is fixed. After that, we seek the values of the linear transformation map ${\bf W}$ and variance $\sigma^2$. These parameters provide a maximal expectation of logarithm likelihood $E[ln p({\bf X}, {\bf Z} | \mu, {\bf W}, \sigma^2)]$.
4. If those changes in parameters are greater than the initial value, then we return to step 2 and seek a new ${\bf Z}$, ${\bf W}$ and $\sigma^2$. Otherwise, we are done.

This way has a few advantages:

1. It is much faster than the exact solution.
2. The solution with the EM-algorithm can handle and restore missed values in our observations with a little modification.
3. We can use the estimation of logarithm likelihood and variance to assess the quality of the result. Read paragraph 12.2 in Pattern recognition and machine learning to understand PPCA and EM algorithms better.

Let us consider how we formalised this procedure in Haskell. We introduce PPCA record data type with input and output fields with the Boolean flag on the presence of missed data.

data PPCA = PPCA
{  _noMissedData       :: Bool
, _learningData       :: Matrix D Double
, desiredDimensions   :: Int
, stopParameter       :: Either Int Double
, _variance           :: Double
, _W                  :: Matrix D Double
, _finalExpLikelihood :: Double
, _restoredMatrix     :: Maybe (Matrix D Double)
}

Input parameters:

_noMissedData - If there are no values marked as NaN, then, in the case of True,
we run the fast version of the EM algorithm, which doesn’t try to
restore missed values.
_learningData - The set of observations, matrix $M \times N$
desiredDimensions - The desired dimension of latent space. This number should be less or equal to $M$
stopParameter - This field stores either the number of iterations or maximally allowed
change of elements of ${\bf W}$ matrix between iterations.

Output parameters:

_variance - The final value of $\sigma^2$
_W - The transformation matrix between latent space and observed space
_finalExpLikelihood - Expectation of logarithm likelihood
_restoredMatrix - The matrix with restored values. If there are no missed values in
_learningData, then it will be Nothing.

The function makePPCATypeSafe takes observations, the required dimension of latent space, and termination condition. This function generates random values for ${\bf W}$ and $\sigma^2$. This function also creates matrices with dimensions in their types and runs either emStepsFast or emStepsMissed. Finally, the function transforms type-safe matrices of the result into the usual matrix type and yields PPCA record.

makePPCATypeSafe :: RandomGen gen => Matrix D Double -> Int
-> Either Int Double -> gen -> PPCA

The emStepsFast function takes observations, initial values of the linear transformation matrix ${\bf W}$ and variance $\sigma^2$, and the termination condition. The result is final ${\bf W}$, $\sigma^2$ and expectation of likelihood logarithm. Note that we require some properties of dimensions in the constraint. The function emStepsMissed of the same type is also quite fascinating:

emStepsFast, emStepsMissed :: forall d y1 x1 y2 x2.
(x2 ~ d , y1 ~ y2, (One <= x1) ~ 'True, AllConstrained SingI [y2, x1, d])
=> DimMatrix D y1 x1 Double -> DimMatrix D y2 x2 Double
-> Double -> Either Int Double
-> (DimMatrix D y2 x2 Double, Double, Double, Maybe (DimMatrix D y1 x1 Double))

emStepsMissed also returns the matrix of observations with restored values. Let’s look at the function more closely. It is too huge to show the whole function, so we consider the implementation partially. First of all, let us notice that there are local functions that return matrices which dimensions depend on the elements. For instance:

...
oldWP :: forall i toDel. ((i <= x1) ~ 'True, (toDel <= y1) ~ 'True, SingI i)
=> Proxy i -> Proxy toDel -> DimMatrix D (y1 - toDel) x2 Double
oldWP iP _ = withListOfIndexes @y1 (unknownIndexes (LessEq iP)) (deleteRowsM @toDel oldW)
...

We use this function to create the set of x1 matrices ${\bf OldW}_{present}$. We remove the rows from ${\bf OldW}$ with the same index as the index of unknown value in the $i$-th column of observations matrix for each $i \in {0, \dots, x_1}$ . Here ${\bf OldW}$ is ${\bf W}$(transformation matrix between spaces) from the previous iteration. As a result, we have the matrix with (y1 - toDel) columns, where toDel depends on the number of unknown values in the $i$-th column of unknown values. Its value is unknown at compile-time, but we can ensure the type checker that we checked its property ((toDel <= y1) ~ 'True) using singletons in the same way as we have described before.
LessEq is a constructor of data type LEQThan (x :: Nat) and consists of Proxy i. One may create a value of this type only if $i \leq x$.

Secondly, we may find this is quite a strange piece of code.

expX_ ::forall (i :: Nat). ((i <= x1) ~ 'True ) => Sing i  -> DimMatrix D x2 i Double
expX_ SZ = emptyM :: DimMatrix D x2 Zero Double
expX_ (SS l) = case lemma1 l (Sing :: Sing x1) of LEQ -> withSingI l $(expX_ l) ^++^ ((withDelNumber expXi) (LessEq (Proxy :: Proxy (i - One))))  Here we form the expectation (in terms of probability theory) of missed values and other elements in the presence of such missed values. Of course, we can’t restore the real values of missed cells, this algorithm just finds an expectation of all values. expX_ is a recursive function: at every step of recursion, the function adds a new column to the accumulator. It is a suitable example of work with dependent types. The compiler checks the body of this function and ensures that this function creates a matrix with exactly i columns at runtime stage. On the other hand, there is also lemma1. Why do we need it? Unfortunately, the type checker is not so smart as we are. We should prove such trivial statements as this one: lemma1 :: forall (n :: Nat) (x :: Nat). (('S n <= x) ~ 'True) => Sing n -> Sing x -> (n :<=: x) lemma1 SZ _ = LEQ lemma1 (SS l) (SS k) = case lemma1 l k of LEQ -> LEQ  It is obvious for us that$(n + 1) \leq x$implies$n \leq x\$, but not for the compiler. Of course, we may merely apply unsafeCoerce for similar examples, but we prefer to use it as rarely as possible. Unsafe coercion is not the way for more complicated examples.

We need this proof because at each iteration except the last one, we call this function again on (i -1), but we proved only that i <= x1, not (i - 1) <= x1.

We didn’t use the singletons functionality initially since dimensions of intermediate matrices don’t depend on their values. In other words, these dimensions depend on the input values and applied operations at each step. The case of PPCA with missed data is completely different in this aspect. That’s why we had to use singletons when we were working on this algorithm. A need to infer some form of properties of such dimensions that may depend on intermediate matrices values caused singletons use. By the way, one can verify within the type system quite safely that required property really has a proof as we have already shown above.

#### Summary

We discussed one way to reduce the debugging time and make our programs less error-prone. In this approach, matrix dimensions are lifted to the type level with the use of the Singletons library. At first glance, our solution looks a bit sophisticated. Why? There remains a question about the way to make it less devious and more idiomatic. In other words, we have to recognise the restrictions of Haskell expressive opportunities. What about performance? Also, our approach helps to remove only errors that affect the dimensions of arrays. Can we track other array parameters to reduce a set of possible runtime errors even more? We’ll talk about it in the next part of our article.


text:
# Imperfect Digital Fibre Optic Link Based Cooperative Distributed Antennas with Fractional Frequency Reuse in Multicell Multiuser Networks

Xu, Xinyi, Zhang, Rong, Ghafoor, Salman and Hanzo, Lajos (2011) Imperfect Digital Fibre Optic Link Based Cooperative Distributed Antennas with Fractional Frequency Reuse in Multicell Multiuser Networks. IEEE Transactions on Vehicular Technology

The achievable throughput of the entire cellular area is investigated, when employing fractional frequency reuse techniques in conjunction with realistically modelled imperfect optical fibre aided distributed antenna systems (DAS) operating in a multicell multiuser scenario. Given a fixed total transmit power, a substantial improvement of the cell-edge area's throughput can be achieved without reducing the cell-centre's throughput. The cell-edge's throughput supported in the worst-case direction is significantly enhanced by the cooperative linear transmit processing technique advocated. Explicitly, a cell-edge throughput of $\eta=5$ bits/s/Hz may be maintained for an imperfect optical fibre model, regardless of the specific geographic distribution of the users.

format: plain


text:
# Math Help - Variance

1. ## Variance

A dealer's profit in units of $5,000 on a new automobile is a random variable X having density function f(x,y) = 2(1-x) for -1 <= x <= 1 a) Find the vaiance in the dealer's profit. b) Demonstrate that chebyshev's inequality holds for k = 2 with the density function above. c) What is the probability that the profit exceeds$500?

a) E(2(1-x)) = -4
$\int-1,1 (-2x-1)f(x)dx$ What is f(x) in this problem?
b) How can I show that it holds true?
c) ???

2. Originally Posted by kenshinofkin
A dealer's profit in units of $5,000 on a new automobile is a random variable X having density function f(x,y) = 2(1-x) for -1 <= x <= 1 a) Find the vaiance in the dealer's profit. b) Demonstrate that chebyshev's inequality holds for k = 2 with the density function above. c) What is the probability that the profit exceeds$500?

a) E(2(1-x)) = -4
$\int-1,1 (-2x-1)f(x)dx$ What is f(x) in this problem?
b) How can I show that it holds true?
c) ???
$f(x)=2(1-x)\ x \in [-1,1]$

is not a density as it integrates up to 4 not 1, are you sure that the range is not $[0,1]$. Also it seems unlikely that a negative profit would be acceptable on a new car (even less a mean profit that is negative).

RonL

3. It could be a typo. So if I go with (0,1) am I doing it right so far. f(x) = x?
So what about the other parts of the question.
b) How can I show that it holds true?
Do I do (1,2) which would show a negitive profit?
c) ???
A dealer's profit in units of $5,000 on a new automobile is a random variable X having density function f(x,y) = 2(1-x) for 0 <= x <= 1 Mr F says: I don't know why you have f(x , y) ....? a) Find the vaiance in the dealer's profit. b) Demonstrate that chebyshev's inequality holds for k = 2 with the density function above. [snip] a) E(2(1-x)) = -4 $\int-1,1 (-2x-1)f(x)dx$ What is f(x) in this problem? b) How can I show that it holds true? c) ??? b) Chebyshev's Inequality: $\Pr(|X - \mu| \geq k \sigma) \leq \frac{1}{k^2}$. So you first need to calculate: 1. $\mu = \int x f(x) \, dx = \int_{0}^{1} x [2(1 - x)] \, dx = 2 \int_{0}^{1} x - x^2 \, dx = \frac{1}{3}$. 2. $\sigma^2 = E(X^2) - \mu^2$, where $E(X^2) = \int x^2 f(x) \, dx = \int_{0}^{1} x^2 [2(1 - x)] \, dx = 2 \int_{0}^{1} x^2 - x^3 \, dx = \, .......$ (which will answer part a) by the way). Therefore $\sigma = \frac{1}{3 \sqrt{2}}$. Substitute $\mu = \frac{1}{3}$, $\sigma = \frac{1}{3 \sqrt{2}}$ and k = 2 into the left hand side of Chebyshev's Inequality: $\Pr \left ( \left |X - \frac{1}{3} \right| \geq \frac{\sqrt{2}}{3} \right)$ $= \Pr \left( X \geq \frac{\sqrt{2} + 1}{3} \right)$ $= \int_{(\sqrt{2} + 1)/3}^{1} 2 (1 - x) \, dx = \, .... \leq \frac{1}{4}$ which demonstrates the inequality. Most of this is basic application of routine definitions and formulae. NB: I reserve the right for the arithmetic details to contain errors so make sure you carefully check all numerical results given above. 5. Originally Posted by kenshinofkin A dealer's profit in units of$5,000 on a new automobile is a random variable X having density function
c) What is the probability that the profit exceeds $500? [snip] Note that a profit of$500 is equivalent to $X = \frac{1}{10}$ since X is in units of five thousand dollars.
$\Pr \left( X > \frac{1}{10} \right) = \int_{1/10}^{1} 2 (1 - x) \, dx = \, ....$


text:
## Thomas' Calculus 13th Edition

a) As we know that $\sin t$ is defined for all real numbers. Therefore, it is defined for all $(x,y)$ b) Since, $\ln t$ is defined for positive real numbers, that is, for all (x,y) except for $(0,0)$.


text:
## Monday, July 9, 2012

### Decline and Fall of the Power Curve

When we think of the power curve associated with some statistical test, we usually envisage a curve that looks something like (half or all of) an inverted Normal density. That is, the curve rises smoothly and monotonically from a height equal to the significance level of the test (say 1% or 5%), until eventually it reaches its maximum height of 100%.

The latter value reflects the fact that power is a probability.

But is this picture that invariably comes to mind - and that we see reproduced in all elementary econometrics and statistics texts - really the full story?

Actually - no!

Let's look at a couple of "typical" power curves - one for the case where the alternative hypothesis is one-sided; and one for the case where a two-sided alternative hypothesis is used. In each case, I'll consider a "simple" null hypothesis, and a "composite" alternative hypothesis.

Recalling that the power of a test is the probability of rejecting H0, at the point where H0 is true the power equals the pre-assigned significance level of the test. At all other points in the parameter space the power the probability of rejecting H0, given that this hypothesis is false (in some way or another).

In the following chart, we see the power curve for a particular test for testing H0: θ = θ0, against HA: θ > θ0. Here, θ is a scalar parameter, and the significance level has been chosen to be 5%.
In the next chart, we see the power curve for a test of the hypothesis, H0: θ = θ0, against HA: θ ≠ θ0. This time, the significance level has been chosen to be 10%.
In each case, the power curve exhibits what we'd like to see - namely, a monotonic increase in the rate of rejection of  H0 (i.e., an increase in power) as this null hypothesis becomes more and more false.

Regrettably, not all tests exhibit this desirable property - including some tests that we use in econometrics. The textbook power curves don't always emerge, and this seems to be something that a lot of practitioners are unaware of!

Before looking at some specific examples, note that in some cases the power curve isn't symmetric about the point θ0, as it is in the last graph.

More importantly, some hypothesis tests are what we call "biased". What this means is that for at least some value(s) of the parameter(s), the power curve falls to a level less than the assigned significance level of the test. In the last graph, if the blue line dipped to a height of less than 10%, anywhere (even if it subsequently rose and eventually got to 100%), then the test would be "biased".

Why is this an undesirable characteristic for a test? Well, recall the definitions of the significance level and the power of a test. The significance level is the probability of a Type I error - that is, Pr.[Reject H0 | H0 True]. The power, on the other hand, is one minus the probability of a Type II error - that is, Power = 1 - Pr.[Not Reject H0 | H0 False] = Pr. [Reject H0 | H0 False].

So, if power < significance level, then Pr. [Reject H0 | H0 False] < Pr.[Reject H0 | H0 True]. That is, at least some value(s) of the parameter(s), the probability of taking the correct action is less than the probability of taking the wrong action! We wouldn't want to be in that situation, would we?

Some of the tests that we use in econometrics can be biased in some circumstances. In fact, in some cases the situation is even worse - the power can fall to zero as the null hypothesis becomes more and more false!

Surely not? Unfortunately - yes!

Here are a couple of examples:

The RESET test

In a recent post I noted that Ramsey's (1969) Regression Specification Error Test (RESET) suffers from poor power properties in some circumstances. Although the test statistic is exactly F-distributed if the null hypothesis is true, under the alternative hypothesis its distribution (and hence its power properties) depend on the nature of the model mis-specification, and the choice of additional regressors that are used to augment the basic model for the purposes of testing for an invalid functional form or omitted regressors.

Here is just one example, taken from Ramsey and Gilbert (1972, p.184):
Note that when the sample size (T) is 20 or 30, the power of the RESET test based on the OLS residuals is less than the significance level (α). The test is biased for the chosen values of the parameters.

Similar examples, such as the one depicted below, are reported by DeBenedictis and Giles (1998) in their comparison of the RESET test with their so-called FRESET test. (For more details, see this recent post.)

Here, the two versions of the FRESET test exhibit increasing power as the model becomes increasingly mis-specified in a particular way, while the power function of the corresponding RESET test exhibits very unorthodox characteristics. We see that the latter test is biased over part of the parameter space. An explanation for the non-monotonic forms of the power curve is given by DeBenedictis and Giles (1998, pp. 401, 405).

The Durbin-Watson test

Krämer (1985) shows that in the case of an OLS regression fitted without an intercept, for certain choices of X data the Durbin-Watson test is not only biased, but its power falls to zero when the first-order autocorrelation coefficient (ρ) approaches 1. The following graph is from Krämer (1985, p.367):

Krämer and  Sonnberger (1986, pp.19-22) show that this can also occur as ρ approaches -1 in value.

In other words, just when you really want the test to reject the null hypothesis, the probability of it doing so is zero!

[Of course, the usual bounds for the critical values for the DW test don't apply if you fit the model through the origin, but that's another matter.]

Less extreme examples of declining power for the DW test can occur if the errors are heteroskedastic, even when the model includes an intercept. For example, the following graph is taken from Giles and Small, 1991, p.40), where increasing values of "h" reflect more and more severe heteroskedasticity:

Once again, the DW test performs badly when it is most needed!

So, although the textbook depictions of power curves are helpful in describing some of the characteristics of certain tests, they don't cover all of the situations that we may encounter. This isn't surprising, but it's worth keeping in mind as we go about our day-to-day econometric practice.

Don't presume that all is well!

References

DeBenedictis, L. F. and D. E. A. Giles, 1998. Diagnostic testing in econometrics: Variable addition, RESET, and Fourier approximations. In A. Ullah and D. E. A. Giles (eds.), Handbook of Applied Economic Statistics, Marcel Dekker, New York, 383-417. WP versionfigures.)

Giles, D. E. A. and J. P Small, 1991. The power of the Durbin-Watson test when the errors are heteroscedastic. Economics Letters, 36, 37-41.

Krämer, W., 1985. The power of the Durbin-Watson test for regression without an intercept. Journal of Econometrics, 28, 363-370.

Kr. The Linear Regression Model Under Test, Physica-Verlag, Heidelberg.

Ramsey, J. B., 1969. Tests for specification errors in classical linear least squares regression analysis. Journal of the Royal Statistical Society, Series B, 31, 350–371.

Ramsey, J. and R. Gilbert, 1972. A Monte Carlo study of some small sample properties of tets for specification error. Journal of the American Statistical Association, 67, 180-186.

© 2012, David E. Giles


text:
D. Ezzat and Grid
time limit per test
2.5 seconds
memory limit per test
256 megabytes
input
standard input
output
standard output

Moamen was drawing a grid of $n$ rows and $10^9$ columns containing only digits $0$ and $1$. Ezzat noticed what Moamen was drawing and became interested in the minimum number of rows one needs to remove to make the grid beautiful.

A grid is beautiful if and only if for every two consecutive rows there is at least one column containing $1$ in these two rows.

Ezzat will give you the number of rows $n$, and $m$ segments of the grid that contain digits $1$. Every segment is represented with three integers $i$, $l$, and $r$, where $i$ represents the row number, and $l$ and $r$ represent the first and the last column of the segment in that row.

For example, if $n = 3$, $m = 6$, and the segments are $(1,1,1)$, $(1,7,8)$, $(2,7,7)$, $(2,15,15)$, $(3,1,1)$, $(3,15,15)$, then the grid is:

Your task is to tell Ezzat the minimum number of rows that should be removed to make the grid beautiful.

Input

The first line contains two integers $n$ and $m$ ($1 \le n, m \le 3\cdot10^5$).

Each of the next $m$ lines contains three integers $i$, $l$, and $r$ ($1 \le i \le n$, $1 \le l \le r \le 10^9$). Each of these $m$ lines means that row number $i$ contains digits $1$ in columns from $l$ to $r$, inclusive.

Note that the segments may overlap.

Output

In the first line, print a single integer $k$ — the minimum number of rows that should be removed.

In the second line print $k$ distinct integers $r_1, r_2, \ldots, r_k$, representing the rows that should be removed ($1 \le r_i \le n$), in any order.

If there are multiple answers, print any.

Examples
Input
3 6
1 1 1
1 7 8
2 7 7
2 15 15
3 1 1
3 15 15

Output
0

Input
5 4
1 2 3
2 4 6
3 3 5
5 1 1

Output
3
2 4 5
Note

In the first test case, the grid is the one explained in the problem statement. The grid has the following properties:

1. The $1$-st row and the $2$-nd row have a common $1$ in the column $7$.
2. The $2$-nd row and the $3$-rd row have a common $1$ in the column $15$.
As a result, this grid is beautiful and we do not need to remove any row.

In the second test case, the given grid is as follows:


text:
# Calculus: Integration by substitution and change of variables – #28706

Question: Integrate this function

$\int{\frac{\sec x\tan xdx}{1+4\sec x}}$


text:
26 questions linked to/from Character edge finding
9k views

### How to make the digits of π go around in a spiral like this?

Here is a start. MapIndexed[Text[Reverse[First[RealDigits[Pi,10,252]]][[Tr@#2]],#]&, Table[{t Cos[t],t Sin[t]},{t,0,16Pi,0.2}]]//Graphics
3k views

### “Covering up” text in Graphics

Consider the following code: ...
3k views

### Finding a function that fits the shape of an image

How can I find a function that fits the given shape of an image? Or instead extract a point set from the shape and then find an interpolating function fits the shape. An example image is attached.
6k views

### How to convert a 2D image into a 3D graphics?

I have an image I would like to make into a .dxf and to do this I need a Graphics3D object. Is there anyway I can do this? Can ...
590 views

### How can text-specific antialiasing be disabled in Rasterize?

While tinkering with the code in the Falling Matrix question, I was hoping to improve the rendering speed by making the rasterizations of the text grayscale. I changed the base color of the text to ...
718 views

### Find path through a set of Coordinates

I have a set of coordinates that I need a robot to draw, thus it must take the shortest path along these coordinates. Plotting them looks like this: ...
704 views

### Ideas on how to improve the rendering of the letter B in this 3D region plot?

I have been playing with the RegionPlot3D idea from this question and have been trying to approximate the Gödel, Escher, Bach logo, but I am a little bit stuck on how to improve the rendering of the ...
2k views

### rotating 3d text

Is it possible to create a 3D rotating text like this: animation here. Here is my try so far: ...
420 views

### Plot a alphabetic character in 2D

I was wondering how I can graphically plot an alphabetic character, for example D, in 2 dimension, using mathematica? I was using ListPlot with specific x and y values but it's not looking anything ...
492 views

### Embedding text on an opaque plane in 3D [duplicate]

A simplified specification of what I am trying to accomplish would be to construct a cube each face with a different color and each face having a text label that can be seen only when viewing from the ...
207 views

### Path construction using Nearest shows ill behavior?

I have a dataSet that I'm trying to sort choosing a starting point and going to its nearest neighbor, and then to its nearest neighbor and so on. To do so, I've ...
438 views

### Generating a list of contour pixels for a morphological component

I have a set of pixilated shapes, and after transforming each shape into a morphological component, I want to be able to return the coordinates for pixels that lie on the contour of the shape. More ...
155 views

### Make a glyph using the BezierCurve function

There are a lot of applications that you make a glyph from a scanned image. Mathematica does have fine tools to interpolate curves like the BezierCurve[] function. ...


text:
Ice
• Water makes up more than 60% of ice.
• Ices are believed to cover the surface of a dust core and/or to be physically mixed with dust.

# Papers

• [2022 - ApJS - Quantum Mechanical Simulations of the Radical–Radical Chemistry on Icy Surfaces]
• The radical-radical coupling reactions are not always barrierless on icy surfaces. Each individual reaction should be evaluated individually.
• The switch from D3 to D3(BJ) would lead to different optimized structures of W18 and W33 even if the same functional is used.
• One of the limitation of this paper is that only one reaction site has been considered for the radical-radical reactions on W18 and W33 surfaces. (What is the most realistic way to describe reaction barriers on amorphous surfaces? Would one get a distribution of energy barriers instead of a single value? How to do that?)
• More realistic water cluster models other than W33 are needed in the future and MD will also be helpful to provide more insights into the reactions on icy surfaces.
• [2021 - A&A Germán Molpeceres et al. Binding energies and sticking coefficients of H2 on crystalline and amorphous CO ice]
• ortho-para spin conversion in H2
• Quantities governing the fraction of molecules that return to the gas phase after a collision with an ice surface are sticking coefficients and residence times.
• The sticking coefficient represents the fraction of molecules that remains adsorbed after a collision.
• Residence times quantify the time that a particular adsorbate stays on a surface after adsorption.
• Sampling is based on GFN-FF simulations at 20K and 1000K with a Berendsen thermostat.
• BHLYP-D4 was chosen as the reference method because it offered good description of CO-CO and CO-H2 interactions compared with CCSD(T)-F12/cc-pVTZ-F12
• Rigid scan at different CO-H2 distances is used as the validation of neural network potentials
• [2020 - ApJ - Herbert M. Urbassek et.al.]: Ejection of Glycine Molecules Adsorbed on a Water Ice Surface by Swift-heavy Ion Irradiation (MD-irradiation)
• [2020 - PCCP - Germán Molpeceres and Johannes Kästner]: Adsorption of H2 on amorphous solid water studied with molecular dynamics simulations (QM/MM, GFN2-xTB)
• Sticking coefficients (from 0 to 1, fraction of molecules sticking on surface after a collision) of H2 depends on H2 kinetic energy and the surface temperature, hardly on the incident angle
• Methods for calculating sticking coefficients: analytical model, molecular dynamics (many studies on H, CO, few on H2)
• The surface of amorphous ice is simulated by taking a hemispherical clusters from 18937 water molecules in a periodic cubic cell.
• [2020 - Nat Astro - Alexey Potapov et.al.]: Dust/ice mixing in cold regions and solid-state water in the diffuse interstellar medium
• A substantial fraction of solid water may be mixed with silicate dust grain in the diffuse ISM, protostellar envelopes and protoplanetary disks.
• The desorption temperature of water ice in laboratory is 160 - 180K, depending on the ice thickness and the heating rate.
• The strongest spectral variations can be seen in the 3.1 $\mu m$ (3225.8 cm $^{-1}$) water ice band which provides the cleanest measure of the H2O ice column density in the astrophysical environments.
• Mixing H2O IR spectra at 10K and 150K and comparing with observation is used for determining relative abundance of low-temperature ice and high-temperature ice
• Mixing pure H2O spectra at 10K and 150K: more than 80% ice in protostellar envelopes and protoplanetary disk is low-temperature ice
• Mixing the silicate/ice spectra at 10K and 150K: the low-temperature ice accounts for only about 30-50% of the column mass toward the investigated objects.
• The presence of solid-water in the diffuse medium (where water molecules could be embedded in silicates) is validated by matching 6.2 $\mu m$ water band in the laboratory 200K spectrum and the band in the Spitzer spectrum
• [2016 - PCCP - Martin R. S. McCoustra et.al.]: Peeling the astronomical onion
• [2014 - A&A - Combined quantum chemical and modeling study of CO hydrogenation on water ice]
• I assume that BHLYP (50 % HF) is the same as BHandHLYP
• [2004 - J. Phys. Chem. A - Performance of Density Functionals for Calculating Barrier Heights of Chemical Reactions Relevant to Astrophysics]
• BHandHLYP has 50% HF

## CO2

A way to build CO2 crystal in ase is

## http://rruff.geo.arizona.edu/AMS/CIF_text_files/11286_cif.txt
from ase.spacegroup import crystal
a = 5.624
co2 = crystal(['C', 'O'], [(0, 0, 0), (0.1185, 0.1185, 0.1185)], spacegroup='Pa-3', cellpar=[a, a, a, 90, 90, 90])

## Others

https://www.nature.com/articles/s41467-020-15377-8 vdW interactions are important to water adsorption on surfaces, but have minor effects on the binding geometries

# Talks

## 2020-06 - Sergio Ioppolo - Infrared Resonant Vibrationally Induced Restructuring of Amorphous Solid Water

What we want in experiments are intense lights with tunable frequencies. Pulses are needed as well


text:
# Noisy Matrix Completion: Understanding Statistical Guarantees for Convex Relaxation via Nonconvex Optimization

20 Feb 2019Yuxin ChenYuejie ChiJianqing FanCong MaYuling Yan

This paper studies noisy low-rank matrix completion: given partial and noisy entries of a large low-rank matrix, the goal is to estimate the underlying matrix faithfully and efficiently. Arguably one of the most popular paradigms to tackle this problem is convex relaxation, which achieves remarkable efficacy in practice... (read more)

PDF Abstract


text:
## Intermediate Algebra for College Students (7th Edition)

The budget can be represented by the formula $x+658.6$


text:
A A
Connect with us:

# Quantum measurements constrained by symmetry

Playing this video requires the latest flash player from Adobe.

## Recording Details

Speaker(s):
Scientific Areas:
Collection/Series:
PIRSA Number:
13040124

## Abstract

The Wigner-Araki-Yanase (WAY) theorem delineates
circumstances under which a class of quantum measurements is ruled out.
Specifically, it states that any observable (given as a self adjoint operator)
not commuting with an additive conserved quantity of a quantum system and
measuring apparatus combined admits no repeatable measurements. I'll review the
content of this theorem and present some new work which generalises and
strengthens the existing results.

The observation that the WAY
constraint vanishes if the observable-to-be-measured is relativised'' (in a
suitable sense) points to interesting links with quantum reference frames and
superselection rules. I'll discuss some of these connections and raise some
open questions.


text:
# mathlibdocumentation

group_theory.free_product

# The free product of groups or monoids #

Given an ι-indexed family M of monoids, we define their free product (categorical coproduct) free_product M. When ι and all M i have decidable equality, the free product bijects with the type word M of reduced words. This bijection is constructed by defining an action of free_product M on word M.

When M i are all groups, free_product M is also a group (and the coproduct in the category of groups).

## Main definitions #

• free_product M: the free product, defined as a quotient of a free monoid.
• free_product.of {i} : M i →* free_product M.
• free_product.lift : (Π {i}, M i →* N) ≃ (free_product M →* N): the universal property.
• free_product.word M: the type of reduced words.
• free_product.word.equiv M : free_product M ≃ word M.

## Remarks #

There are many answers to the question "what is the free product of a family M of monoids?", and they are all equivalent but not obviously equivalent. We provide two answers. The first, almost tautological answer is given by free_product M, which is a quotient of the type of words in the alphabet Σ i, M i. It's straightforward to define and easy to prove its universal property. But this answer is not completely satisfactory, because it's difficult to tell when two elements x y : free_product M are distinct since free_product M is defined as a quotient.

The second, maximally efficient answer is given by word M. An element of word M is a word in the alphabet Σ i, M i, where the letter ⟨i, 1⟩ doesn't occur and no adjacent letters share an index i. Since we only work with reduced words, there is no need for quotienting, and it is easy to tell when two elements are distinct. However it's not obvious that this is even a monoid!

We prove that every element of free_product M can be represented by a unique reduced word, i.e. free_product M and word M are equivalent types. This means that word M can be given a monoid structure, and it lets us tell when two elements of free_product M are distinct.

There is also a completely tautological, maximally inefficient answer given by algebra.category.Mon.colimits. Whereas free_product M at least ensures that (any instance of) associativity holds by reflexivity, in this answer associativity holds because of quotienting. Yet another answer, which is constructively more satisfying, could be obtained by showing that free_product.rel is confluent.

## References #

van der Waerden, Free products of groups

inductive free_product.rel {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
free_monoid (Σ (i : ι), M i)free_monoid (Σ (i : ι), M i) → Prop

A relation on the free monoid on alphabet Σ i, M i, relating ⟨i, 1⟩ with 1 and ⟨i, x⟩ * ⟨i, y⟩ with ⟨i, x * y⟩.

def free_product {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
Type (max u_1 u_2)

The free product (categorical coproduct) of an indexed family of monoids.

Equations
@[protected, instance]
def free_product.inhabited {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
@[protected, instance]
def free_product.monoid {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
theorem free_product.word.ext_iff {ι : Type u_1} {M : ι → Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} (x y : free_product.word M) :
theorem free_product.word.ext {ι : Type u_1} {M : ι → Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} (x y : free_product.word M) (h : x.to_list = y.to_list) :
x = y
@[ext]
structure free_product.word {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
Type (max u_1 u_2)

The type of reduced words. A reduced word cannot contain a letter 1, and no two adjacent letters can come from the same summand.

def free_product.of {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {i : ι} :
M i →*

The inclusion of a summand into the free product.

Equations
theorem free_product.of_apply {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {i : ι} (m : M i) :
@[ext]
theorem free_product.ext_hom {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f g : →* N) (h : ∀ (i : ι), ) :
f = g
def free_product.lift {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] :
(Π (i : ι), M i →* N) →* N)

A map out of the free product corresponds to a family of maps out of the summands. This is the universal property of the free product, charaterizing it as a categorical coproduct.

Equations
@[simp]
theorem free_product.lift_symm_apply {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f : →* N) (i : ι) :
@[simp]
theorem free_product.lift_of {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (fi : Π (i : ι), M i →* N) {i : ι} (m : M i) :
= (fi i) m
theorem free_product.induction_on {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {C : → Prop} (m : free_product M) (h_one : C 1) (h_of : ∀ (i : ι) (m : M i), C ) (h_mul : ∀ (x y : , C xC yC (x * y)) :
C m
theorem free_product.of_left_inverse {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [decidable_eq ι] (i : ι) :
theorem free_product.of_injective {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] (i : ι) :
@[protected, instance]
def free_product.has_inv {ι : Type u_1} (G : ι → Type u_4) [Π (i : ι), group (G i)] :
Equations
theorem free_product.inv_def {ι : Type u_1} (G : ι → Type u_4) [Π (i : ι), group (G i)] (x : free_product G) :
@[protected, instance]
def free_product.group {ι : Type u_1} (G : ι → Type u_4) [Π (i : ι), group (G i)] :
Equations
def free_product.word.empty {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] :

The empty reduced word.

Equations
@[protected, instance]
def free_product.word.inhabited {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] :
Equations
def free_product.word.prod {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] (w : free_product.word M) :

A reduced word determines an element of the free product, given by multiplication.

Equations
@[simp]
theorem free_product.word.prod_nil {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] :
def free_product.word.fst_idx {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] (w : free_product.word M) :

fst_idx w is some i if the first letter of w is ⟨i, m⟩ with m : M i. If w is empty then it's none.

Equations
theorem free_product.word.fst_idx_ne_iff {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {w : free_product.word M} {i : ι} :
w.fst_idx some i ∀ (l : Σ (i : ι), M i), l w.to_list.head'i l.fst
theorem free_product.word.pair.ext_iff {ι : Type u_1} {M : ι → Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} {i : ι} (x y : i) :
@[ext]
structure free_product.word.pair {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] (i : ι) :
Type (max u_1 u_2)

Given an index i : ι, pair M i is the type of pairs (head, tail) where head : M i and tail : word M, subject to the constraint that first letter of tail can't be ⟨i, m⟩. By prepending head to tail, one obtains a new word. We'll show that any word can be uniquely obtained in this way.

theorem free_product.word.pair.ext {ι : Type u_1} {M : ι → Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} {i : ι} (x y : i) (h : x.head = y.head) (h_1 : x.tail = y.tail) :
x = y
@[protected, instance]
def free_product.word.pair.inhabited {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] (i : ι) :
Equations
def free_product.word.rcons {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} (p : i) :

Given a pair (head, tail), we can form a word by prepending head to tail, except if head is 1 : M i then we have to just return word since we need the result to be reduced.

Equations
theorem free_product.word.cons_eq_rcons {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} {m : M i} {ls : list (Σ (i : ι), M i)} {h1 : ∀ (l : Σ (i : ι), M i), l i, m⟩ :: lsl.snd 1} {h2 : list.chain' (λ (l l' : Σ (i : ι), M i), l.fst l'.fst) (i, m⟩ :: ls)} :
{to_list := i, m⟩ :: ls, ne_one := h1, chain_ne := h2} = free_product.word.rcons {head := m, tail := mk_aux ls h1 h2, fst_idx_ne := _}
@[simp]
theorem free_product.word.prod_rcons {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} (p : i) :
theorem free_product.word.rcons_inj {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} :
def free_product.word.equiv_pair {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) :

The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing the first letter if it comes from M i. Given a pair, it prepends the head to the tail.

Equations
theorem free_product.word.equiv_pair_symm {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) (p : i) :
theorem free_product.word.equiv_pair_eq_of_fst_idx_ne {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {i : ι} {w : free_product.word M} (h : w.fst_idx some i) :
= {head := 1, tail := w, fst_idx_ne := h}
@[protected, instance]
def free_product.word.summand_action {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) :
mul_action (M i)
Equations
@[protected, instance]
def free_product.word.mul_action {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations
theorem free_product.word.of_smul_def {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) (w : free_product.word M) (m : M i) :
theorem free_product.word.cons_eq_smul {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {i : ι} {m : M i} {ls : list (Σ (i : ι), M i)} {h1 : ∀ (l : Σ (i : ι), M i), l i, m⟩ :: lsl.snd 1} {h2 : list.chain' (λ (l l' : Σ (i : ι), M i), l.fst l'.fst) (i, m⟩ :: ls)} :
{to_list := i, m⟩ :: ls, ne_one := h1, chain_ne := h2} = mk_aux ls h1 h2
theorem free_product.word.smul_induction {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {C : → Prop} (h_empty : C free_product.word.empty) (h_smul : ∀ (i : ι) (m : M i) (w : , C wC w)) (w : free_product.word M) :
C w
@[simp]
theorem free_product.word.prod_smul {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (m : free_product M) (w : free_product.word M) :
(m w).prod = m * w.prod
def free_product.word.equiv {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :

Each element of the free product corresponds to a unique reduced word.

Equations
@[protected, instance]
def free_product.word.decidable_eq {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations
@[protected, instance]
def free_product.word.free_product.decidable_eq {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations


text:
# Convexity of the variance of a mixture distribution

$$X$$ is a random variable that is sampled from the mixture of uniform distributions. In other words: $$X \sim \sum_{i=1}^N w_i \cdot \mathbb{U}(x_i, x_{i+1}),$$ where $$\mathbb{U}(x_i, x_{i+1})$$ denotes a random variable that follows a uniform distribution in $$[x_i, x_{i+1}]$$. For feasibility, we need $$w \geq 0, \ \sum_{i=1}^N w_i = 1$$.

In an optimization problem my variables are $$w_i$$ for $$i=1,\ldots,N$$, and I would like to upper bound the variance of $$X$$. According to Wikipedia, the variance of $$X$$ is: $$\mathrm{Var}(X) = \sum_{i=1}^N w_i(\sigma_i^2+ \mu_i^2 - \mu^2)$$ where $$\sigma_i^2$$ and $$\mu_i$$ are the variance and mean of $$\mathbb{U}(x_i, x_{i+1})$$, respectively (which are parameters), and $$\mu$$ is the mean of the mixture, which is $$\mu = \sum_{i=1}^N w_i \frac{x_i + x_{i+1}}{2}.$$

Thus, if my derivation is not wrong: $$\mathrm{Var}(X) = \sum_{i=1}^N w_i\left(\sigma_i^2+ \mu_i^2 - \left(\sum_{j=1}^N w_j \frac{x_j + x_{j+1}}{2}\right)^2\right)$$ which is very ugly and appears to be non-convex to upper bound this function (edit: I want to constrain $$\mathrm{Var}(X) \leq \mathrm{constant}$$).

My question is, is there any trick, or any other convex approximation of such a variance, such that I can include an upper bound on the variance constraint?

• Just for completion: in terms of only $w_i$ and $x_i$ the variance is given by $$\frac13\sum_{i=1}^Nw_i(x_i^2+x_ix_{i+1}+x_{i+1}^2)-\frac14\left(\sum_{i=1}^Nw_i(x_i+x_{i+1})\right)^2.$$ Unfortunately using Cauchy-Schwarz on the last term yields a lower bound. – TheSimpliFire Jul 30 '20 at 6:39
• @TheSimpliFire thanks! How do you not have $w_i^3$ terms? – independentvariable Jul 30 '20 at 13:02
• You can remove the $w_i^3$ terms by taking $\mu$ out of the summation and using that $\sum_i w_i = 1$. The Wikipedia link you provided makes the same step. – Kevin Dalmeijer Jul 30 '20 at 19:10
• The Wikipedia formula for the variance looks wrong to me. Assuming the component random variables are independent, shouldn't the variance of $X$ be $\sum_i w_i^2 \sigma_i^2$? – prubin Jul 30 '20 at 21:58
• @independentvariable Sorry, I was misled by your first formula. What I wrote was the variance of the weighted sum of the uniform variables. A mixture distribution is not a weighted sum of independent variables, though. Rather, you pick one of the variables randomly based on the weights and the get an observation of that variable. – prubin Jul 31 '20 at 15:51

In order to find the best upper bound for variance, for given input values of $$u_i$$ and $$\sigma_i^2$$, you should globally maximize variance with respect to the $$w_i$$, subject to the constraints $$w_i \ge 0, \Sigma w_i = 1$$.

This can be formulated as a convex QP (Quadratic Programming problem), i.e., maximizing a concave quadratic subject to linear constraints. Hence it is easy to solve, unless $$n$$ is gigantic, which hardly seems likely for any reasonable mixture distribution. I leave to the OP as an exercise, whether the KKT conditions can yield a closed form solution.

The convex QP takes the form:

maximize $$(\Sigma_{i=1}^n w_i (\sigma_i^2 +\mu_i^2)) - \mu^2$$ with respect to $$\mu, w_i$$

subject to $$\Sigma_{i=1}^n w_i \mu_i = \mu, w_i \ge 0 \forall i, \Sigma_{i=1}^n w_i = 1$$.

If all $$u_i$$ are equal to each other, this would be a Linear Programming problem with compact constraints. Therefore the optimum would be at a vertex of the constraints, and in this case, that vertex would be $$w_i = 1$$ for the $$i$$ corresponding to the largest $$\sigma_i^2$$, and all other $$w_i = 0$$.

Edit: In response to edit to question: "I want to constrain Var(X) $$\le$$ constant)"

If the naive approach of adding the constraint Var(X) $$\le$$ constant to my above convex QP formulation were performed, that would add a non-convex quadratic constraint, making the problem a non-convex Quadratically-Constrained Quadratic Program (QCQP), which requires a global optimizer, such as Gurobi 9.x or BARON to solve to global optimality.

However, there is an easier, faster method: Solve the (pre-Edit) convex QP formulation. Then maximum variance, accounting for the constraint Var(X) $$\le$$ constant), equals

min(optimal objective value of convex QP formulation,constant).

• Many thanks for your reply! Before going to the direction of an upper bound, I want to make sure whether the Wikipedia formula is correct. I think user prubin's answer is also given here without any common mean assumption: theanalysisofdata.com/probability/…. – independentvariable Jul 31 '20 at 9:52
• @prubin is usually correct, but not on this. Your link, theanalysisofdata.com is just flat out wrong., Don't believe me? Try a simulation. Handy formula: Variance = mean of conditional variance + variance of conditional mean. The 2nd of these terms is affected by how common or not the $\mu_i$ are. The linked (and prubin's) formula is incorrect even if $n = 2, w_1 = w_2 = 1/2, \mu_1 = \mu_2 = 0, \sigma_1^2 = 1, \sigma_2^2 = 1$. In that case, variance = 1, but linked and prubin's formula gives variance = 1/2. – Mark L. Stone Jul 31 '20 at 11:37
• Yes, Wikipedia's formulas are correct. You can verify by simulation if you don't trust your analytical skills. I made use of Wikipedia's formulas in my QP formulation, but I cleverly didn't substitute everything into the objective rather, added linear constraint for $\mu$. – Mark L. Stone Jul 31 '20 at 11:45
• I don't completely understand the easier, faster method. Also, I'm a bit sceptical because the Var($X$) $\le$ constant has a non-convex feasible region in $w$, which seems difficult to avoid. – Kevin Dalmeijer Jul 31 '20 at 18:28
• If the optimal objective value of the convex QP is > "constant", the max variance constraint is non-binding. If "constant" $\le$ optimal objective value of convex QP, then by continuity of the objective function with respect to $w_i$, the optimal objective value (i.e., max variance) with the max variance constraint is "constant". QED. Continuity is the key to sneaking around the non-convexity. – Mark L. Stone Jul 31 '20 at 20:31


text:
# "value" entries

## Expect no, but fight for yes

### At the end of the day, there are no rules, only guidelines.

Editor’s note: this is the transcript of DJ Patil’s commencement address to the 2014 graduating class at UC Santa Cruz’s Jack Baskin School of Engineering; it is published here with permission.

DJ Patil with his father. Photo: courtesy of DJ Patil.

Thank you, Dean Ramirez and the distinguished faculty here today. And thank you to all the friends and family who have come out to celebrate this day. Thank you all for being here.

But most importantly: you. The Class of 2014. I gotta tell you guys: you look awesome. Downright amazing.

Now, I recognize that I’m the person standing between you and a selfie with your diploma, so I’m going to do my best to keep it short. And to start, I’m going to start with a confession: ever since Professor Getoor reached out and asked me if I’d be willing to do this, I’ve been dreading it. I mean really, really dreading it. I mean like as in final-exam-in-compilers dreading it. Read more…

## Where will software and hardware meet?

### Software is adding more and more value to machines. Could it completely commoditize them?

I’m a sucker for a good plant tour, and I had a really good one last week when Jim Stogdill and I visited K. Venkatesh Prasad at Ford Motor in Dearborn, Mich. I gave a seminar and we talked at length about Ford’s OpenXC program and its approach to building software platforms.

The highlight of the visit was seeing the scale of Ford’s operation, and particularly the scale of its research and development organization. Prasad’s building is a half-mile into Ford’s vast research and engineering campus. It’s an endless grid of wet labs like you’d see at a university: test tubes and robots all over the place; separate labs for adhesives, textiles, vibration dampening; machines for evaluating what’s in reach for different-sized people.

Prasad explained that much of the R&D that goes into a car is conducted at suppliers–Ford might ask its steel supplier to come up with a lighter, stronger alloy, for instance–but Ford is responsible for integrative research: figuring out how to, say, bond its foam insulation onto that new alloy.

In our more fevered moments, we on the software side of things tend to foresee every problem being reduced to a generic software problem, solvable with brute-force computing and standard machinery. In that interpretation, a theoretical Google car operating system–one that would drive the car and provide Web-based services to passengers–could commoditize the mechanical aspects of the automobile. Read more…

## The media-marketing merge

### Can good content come from pay-to-play relationships?

I ran across a program Forbes is running called BrandVoice that gives marketers a place on Forbes’ digital platform. During a brief audio interview with TheMediaBriefing, Forbes European managing director Charles Yardley explained how BrandVoice works:

“It’s quite simply a tenancy fee. A licensing fee that the marketer pays every single month. It’s based on a minimum of a six-month commitment. There’s two different tiers, a $50,000-per-month level and a$75,000-per-month level.” [Discussed at the 4:12 mark.]

Take a look at some of the views BrandVoice companies are getting. You can see why marketers would be interested. Read more…

## Building conference programs: it’s about the attendee

### The essential principles of conference development.

I’ve chaired computer industry conferences for ten years now. First for IDEAlliance (XML Europe, XTech), and recently with O’Reilly Media (OSCON, Strata). Over the years I have tried to balance three factors as I select talks: proposal quality, important new work, and practical value of the knowledge to the attendees.

As the competition for speaking slots at both Strata and OSCON reach intense levels, I wanted to articulate these factors, and the principles I use when compiling conference programs.

## How the program is made

My guiding principle in putting a program together is value to the attendees. They’re why we do this. By putting out quality content and speakers, we attract thinking, interested attendees. In turn, our sponsors get a much better quality of conversation and customer contact through their presence at the event.

Here’s the process in a nutshell: proposals are invited through a public call for participation, and then reviewers, drawn from the industry community of experts, will grade and comment on each proposal. I and my co-chairs use this feedback, along with editorial judgement, to compile the final schedule. For keynotes, and a small number of breakout sessions, we will augment the review process by inviting talks we think are important for the program.


text:
#### Vol. 12, No. 8, 2019

 Recent Issues
 The Journal About the Journal Editorial Board Editors’ Interests Subscriptions Submission Guidelines Submission Form Policies for Authors Ethics Statement ISSN: 1944-4184 (e-only) ISSN: 1944-4176 (print) Author Index Coming Soon Other MSP Journals
The supersingularity of Hurwitz curves

### Erin Dawson, Henry Frauenhoff, Michael Lynch, Amethyst Price, Seamus Somerstep, Eric Work, Dean Bisogno and Rachel Pries

Vol. 12 (2019), No. 8, 1293–1306
##### Abstract

We study when Hurwitz curves are supersingular. Specifically, we show that the curve ${H}_{n,\ell }:{X}^{n}{Y}^{\ell }+{Y}^{n}{Z}^{\ell }+{Z}^{n}{X}^{\ell }=0$, with $n$ and $\ell$ relatively prime, is supersingular over the finite field ${\mathbb{F}}_{p}$ if and only if there exists an integer $i$ such that ${p}^{i}\equiv -1\phantom{\rule{0.2em}{0ex}}mod\phantom{\rule{0.2em}{0ex}}\left({n}^{2}-n\ell +{\ell }^{2}\right)$. If this holds, we prove that it is also true that the curve is maximal over ${\mathbb{F}}_{{p}^{2i}}$. Further, we provide a complete table of supersingular Hurwitz curves of genus less than 5 for characteristic less than 37.

However, your active subscription may be available on Project Euclid at
https://projecteuclid.org/involve

We have not been able to recognize your IP address 3.229.142.91 as that of a subscriber to this journal.
Online access to the content of recent issues is by subscription, or purchase of single articles.

or by using our contact form.

##### Keywords
Hurwitz curve, Hasse–Weil bound, maximal curve, minimal curve, Fermat curve, supersingular curve
##### Mathematical Subject Classification 2010
Primary: 11G20, 11M38, 14H37, 14H45, 11E81
Secondary: 11G10, 14H40, 14K15


text:
1. anonymous

2. anonymous

can you help me?

3. anonymous

@e.mccormick

4. e.mccormick

OK, so, what are some ways to prove two traingles are congruent? You want one of them as a goal.

5. anonymous

alright

6. e.mccormick

There are 5 ways. sss, sas, asa, aas, and hl. The last only applies in right triangles: http://www.regentsprep.org/regents/math/geometry/gp4/ltriangles.htm You need to move toward one of those. So you need to take what is given and show how it applies to parts of those, then use other rules to fill in mising bits. For example, it says D is the midpoint of AC. By the definiton of a midpoint that means AD = DC. So that means antyhing wih a side might use that.

7. anonymous

okat its starting to make sense but how to do i put that into proof , statements and reasons?

8. e.mccormick

"By definition, a midpoint of a line segment is the point on that line segment that divides the segment two congruent segments." from http://www.regentsprep.org/regents/math/geometry/gcg2/lmidpoint.htm As I said you use the definition of midpoint to prove that one. What other sides can you prove would have the same measure?

9. anonymous

um so i use the definition as my proof? cbd would have the same measurements

10. e.mccormick

You use the "definition of midpoint" for the reason for that one part, ad = dc cbd? Do you mean the angle? I asked about sides at this point.

11. anonymous

im confused on how to do this paper i dont get what your explaining i cant figure it out so i can write it down

12. e.mccormick

Well, like I said, you have only 5 ways you can prove two triangles are congruent. So you must prove each part of one of those 5, then you can prove that 5.

13. anonymous

okay i get that so for proof for the 1st one i put AD = DC

14. e.mccormick

Well, usually you start by listing the given you would use first. So you need "D us midpoint of AC" and "Given" Then for the 2nd one you can use AD = DC, definition of midpoint.

15. anonymous

proof is D is midpoint of Ac wait im so lost uggghhhhhhh how am i ever gonna finish this stupid paper

16. e.mccormick

It is just a couple more. See, there are three sides, right? And SSS is a proof of congruance. In two lines you just proved one side. So, how would you prove a second side?

17. anonymous

i dont know

18. e.mccormick

Well, what ese is given?

19. anonymous

CD?

20. e.mccormick

There are two givens and a diagram: ABC is isosceles D is the midpoint of AC. We already used "D is the midpoint of AC." so what can you get from "ABC is isosceles"

21. anonymous

BC

22. e.mccormick

BC is what?

23. anonymous

BC = AC?

24. anonymous

or A is the midpoint to BC

25. e.mccormick

No. Not BC = AC. Which sides on the diagram have the same mark?

26. e.mccormick

BC and...?

27. anonymous

BA?

28. e.mccormick

Yes. So the 3rd line is ABC is isosceles, given BC = BA, definition of isosceles

29. e.mccormick

Well, 3rd and 4th lines.

30. e.mccormick

OK, so that covers 2 of the sides. One more side and you prove SSS works. So what is the last side you need?

31. anonymous

DB?

32. e.mccormick

Yes. And DB is a shared side! So it is the same thing. There is a tecnical name for this: Reflexive Property of Equality http://www.mathwords.com/r/reflexive_property.htm The reflective property basically says that everything is itself. It is sstupid, but math actually has a rule to prove this! So the 5th line is: DB = DB, Reflexive Property of Equality

33. anonymous

is that it?

34. e.mccormick

One last line. The SSS line. ADB = CDB, SSS

35. anonymous

okay?

36. e.mccormick

And that is it. See, you prove each side, in this case, then say because the sides are = the triangles are =. So you prove each part then the whole. I'll give a plain language example.

37. anonymous

can you write all the lines out in order so first the proof then statements then reasons cause i cant figure out how to write that part

38. anonymous

i know it sounds like a pain but it would help me out

39. e.mccormick

I want to prove I have done my chores. I have a list of do dishes, make bed, and feed cat. I show that my bed is made. I show that the dishes are on the shelves so they mist have been done. I show that the cat bowl is empty... oops. Proves nothing! But I show the cat is happy and not hungry. So I must of fed the cat. All three things are done so the list must have been done. Proof I did my chores. That is what a proof is about. Showing how things have been done and are linked together. The lines for your proof are here, it this post. Just need to copy them in order.

40. anonymous

what?

41. e.mccormick

That is really what proofs are like. Just how you would prove to a parent that you did what you were told to do.

42. anonymous

but what parts do i use to make that proof your not telling me your using english for math and its confusing me .

43. e.mccormick

Well, from the top down in this post, when did I say things would be line(s) in your proof of triangles?

44. anonymous

no where

45. e.mccormick

I did several times...

46. anonymous

maybe but everything you explained is mixed up in different text and im confused and i asked you if you could straighten them out basically because im lost i wouldnt be asking otherwise.

47. e.mccormick

In those

48. anonymous

okay .. can you help me make sure i got these right then?

49. anonymous

so the 1st one is AD = DC as the proof right?

50. e.mccormick

1) D is Midpoint of AC, Given 2) AD = DC, definition of midpoint

51. anonymous

Do you understand how i have to write this paper out as? Proof is one then, statements then, reasons

52. e.mccormick

Yes. That is why I put a comma.

53. e.mccormick

#) statement , reason

54. anonymous

that doesnt make sense there so 3 commas not 2? i need proof as well as statement and reason

55. e.mccormick

$$\begin{array}{lcl} Statements & \qquad & Reasons \\ \hline \text{D is the midpoint of AC} & \qquad & \text{Given} \\ AD = DC & \qquad & \text{Definition of midpoint} \\ \end{array}$$

56. anonymous

57. e.mccormick

Yes. And I am trying to show how it would look when filled out.

58. anonymous

is my proof ABD = CBD

59. anonymous

i know but wheres the proof???

60. e.mccormick

Which is the LAST line. You build up to that.

61. e.mccormick

Those are the first two lines. There are six lines.

62. anonymous

okay can you write out a the lines? ive been trying to write them down and put it together but i cant get em right :/

63. anonymous

ive been working on this paper for days i need to get it done and its just making me upset more and more

64. anonymous

plus i cant figure out what the damn proof is

65. e.mccormick

Those are the only two that were not written out clearly. The first two. The 3rd, 4th, 5th, and 6th are all in that image: http://assets.openstudy.com/updates/attachments/55ef8588e4b0dedaa9edb1a4-e.mccormick-1441830203955-proof.png I did them as: Statment, reason ABC is isosceles, given They are all there.

66. anonymous

but whats the proof what do i write for proof please tell me im going to cry this is ridiculous i cant figure that part out

67. e.mccormick

As I said, it is right there, six lines. All six are typed out.

68. anonymous

k


text:
# Short WritingPromptReview the following documents. How do these two accounts reflect certain points of view? Which source is more reliableand why?

###### Question:

Short Writing Prompt
Review the following documents. How do these two accounts reflect certain points of view? Which source is more reliable
and why? Explain your answer, supporting it with reasons and evidence from the documents.

$Short Writing Prompt Review the following documents. How do these two accounts reflect certain po$

### Choose the word that could fill in the blank based on the adjective being used.Me gustan simpáticos.Las chicasLos chicosLa

Choose the word that could fill in the blank based on the adjective being used. Me gustan simpáticos. Las chicas Los chicos La mujer El hombre...

### Find the products. show your thinking. the first row gives some ideas for showing your thinking pls

Find the products. show your thinking. the first row gives some ideas for showing your thinking pls me solve this ...

### (c) Solve8 + w = 6W =

(c) Solve 8 + w = 6 W =...

### Unit assessment: renaissance through modern buildings is this statement true or false? architects add

Unit assessment: renaissance through modern buildings is this statement true or false? architects add beauty to the buildings where we live, play, work, and worship, to influence how viewers feel while inside or outside the buildings. true or false?...

### What is the purpose of a web, or cluster diagram? to organize information into main ideas and supporting details to chart

What is the purpose of a web, or cluster diagram? to organize information into main ideas and supporting details to chart main points and subtopics to make comparisons between two subjects to present information in a chronological order...

### An equation in the system is y = x + 1. what is the other equation in the system if the solution is

An equation in the system is y = x + 1. what is the other equation in the system if the solution is only at (0, 1)? x − y = 1 2x + 2y = 4 x + y = 0 x + 2y = 2...

### Five countries enter a race. The first three racers in order, Jamaica finished before Barbados, but behind Trinidad. Haiti finished

Five countries enter a race. The first three racers in order, Jamaica finished before Barbados, but behind Trinidad. Haiti finished before Guyana, but behind Barbados. Who won the Bronze (finished in 3rd place)?...

### How many amino acids are necessary for the human body to function properly? A. 22 B. 8-10 C. 12-14 D. Amino acids are not necessary

How many amino acids are necessary for the human body to function properly? A. 22 B. 8-10 C. 12-14 D. Amino acids are not necessary for the human body to function properly....

### How can you showcase your accomplishments best?

How can you showcase your accomplishments best?...

### 3. describe a real or made up but realistic situation in which you would want to use installment credit.

3. describe a real or made up but realistic situation in which you would want to use installment credit. (2-4 sentences. 1.0 points) 4. describe a real or made up but realistic situation in which you would want to use noninstallment credit. (2-4 sentences. 1.0 points) 5. describe a real or made up b...

### Write a rule describing the translation below please!

Write a rule describing the translation below please! $Write a rule describing the translation below please!$...

### Which of the following is not a disadvantage to cash advances on a credit card?a.Cash advances are similar to loans in that they need

Which of the following is not a disadvantage to cash advances on a credit card? a. Cash advances are similar to loans in that they need to be paid back with interest. b. Cash advances require a lot of paperwork and are generally difficult to get. c. Cash advances are often the last thing to be paid...

### What is the theme, subject, speaker, and what are the figure of speeches in 'my father is a simple man'?

What is the theme, subject, speaker, and what are the figure of speeches in "my father is a simple man"? (poem is written by luis omar salinas) will mark brainliest...

### The extremes in this proportion 3/4=15/20 are

The extremes in this proportion 3/4=15/20 are...

### What is the power in a circuit that uses 3v and 5.6ma?

What is the power in a circuit that uses 3v and 5.6ma?...

### Can someone pls helpThe Nile River allowed the Egyptians to .A) travel and then trade for goodsB) remain untouched by other culturesC)

Can someone pls help The Nile River allowed the Egyptians to . A) travel and then trade for goods B) remain untouched by other cultures C) grow thick forests...

### Let f(x)=x^2+6x+11 what is the average rate of change from x=5 to x=8

Let f(x)=x^2+6x+11 what is the average rate of change from x=5 to x=8...

### Does anyone have the answers for the End of Semester Test: Health Science 2B on Plato/Edmentum??

Does anyone have the answers for the End of Semester Test: Health Science 2B on Plato/Edmentum??...
Please help with the first one :) $Please help with the first one :)$...


text:
CMU 15-418/618 (Spring 2013) Final Project:

Molecular Dynamics Simulations on a GPU

Project Summary

The goal of this project was do develop an effective molecular dynamics simulation in OpenCL to be run on a GPU. Specifically, the focus was on strategies to divide the work of computing the pairwise force interaction between particles. For molecular dynamics, the primary interaction of interest is the Van Der Waals interaction between atoms. I chose to use the relatively simple Lennard Jones potential to model this interaction. The simulation is rendered in OpenGL to visualize the simulation. In the end, I chose to keep each individual simulation very simple and short so that I could analyze its performance over a wide range of parameters. A demonstration of this project would take the form of a video capture instead of a live demo, since I likely won't have a chance to get everything up and running on my laptop (which has inferior power anyway). Since I ran simulations under a wide variety of scenarios, my discussion will be focused on those results.

Background

The problem being solved here is fundamentally identical to an n-body simulation--the only difference is the force of interest. The simulation has two steps: first update forces and then update positions, repeat forever. Updating positions is trivial, since you just need to move each particle based on its current force value. Updating the forces is the interesting part.

In both cases, all $n$ objects interact separately will all $n-1$ other objects, meaning that $O(n^2)$ distinct calculations are required. Therefore, the topic of interest is whether they can be broken up in some manner to allow them to be done faster. Similarly, a common simplification of the problem is to ignore interactions beyond a certain distance, meaning that there are several possibilities to explore.

As far as the physics of the problem goes, I'm making a number of simplifying assumptions so that I can focus on the computer science aspect of the problem. One is that all particles are identical (specifically, they're all Xenon atoms). The Lennard Jones potential has two parameters that depend on the particle. The depth of the potential well, equivalently the strength of the interaction, is given by $\epsilon$. The distance that is energetically most favorable is based on $\sigma$. For Xenon, these are $\epsilon = 1.77$ kJ/mol and $\sigma = 4.10$ Angstroms. I don't think that adding support for a heterogeneous group of atoms would add much from the computer science perspective. The force calculation is $$F_{lj}(r) = 24 \epsilon \left[2\frac{\sigma^{12}}{r^{13}} - \frac{\sigma^{6}}{r^{7}}\right]$$ In other words, attractive beyond a certain distance and repulsive within it. This is illustrated in the image below.

Image credit to the UCDavis ChemWiki

Finally, I chose OpenCL for this project because it seems like most of the work done in this area in the past has been to implement parallelism with things like MPI as opposed to GPGPU and SIMD. This seems like a reasonable approach, since the there aren't any data dependencies or critical regions within the force update itself. There's also no communication step to worry about. However, in the context of ignoring long range interactions, divergence may become an issue.

Approach

The naive solution is to consider each particle separately and loop over all other particles to produce the combined force and store the result. Sadly, this doesn't even allow you to take advantage of the symmetry of the problem in any sensible manner. I spent some time on this issue, but the lack of support atomic operations on floats (or float4s) left me with no sensible solution. This approach will be referred to as parallelism over particles.

An alternate approach is parallelism over forces. Although the same amount of work is done, the fundamental difference with this approach is that we can take advantage of memory locality to compute the forces in square tiles (size $p \times p$). Since these tiles all need the same particle positions, they can be loaded into shared memory (the __local address space, in OpenCL terms). So, a further topic of interest brought up in this approach is how large the tile should be. In OpenCL terms, this would be the size of the local group (equivalent to the block size in CUDA terms). A demonstration of how this is broken down is shown below.

Image credit to NVIDIA.

As mentioned previously, another method to improve the speed of the computation (at the expense of accuracy though) is to ignore long range interactions by making them all 0. With all of these possibilities in mind, I wrote four different kernel functions to update the forces.

1. force_naive: Consider each particle separately and loop over all others.
2. force_naive_clip: Similar to above, but ignore things more than 10 angstroms away.
3. force_tile: Implement the tiling algorithm.
4. force_tile_clip: Like the previous one, but ignores anything more than 10 angstroms away.

Originally, I had planned on using a third strategy of spatial decomposition, where particles are binned and only interactions with adjacent bins are computed. This would improve on the above methods by not even considering particles that are far away (in the above kernels, you still need to look at everyone else, even if you proceed to ignore them). I ended up abandoning this strategy because I couldn't find a suitable way to implement this using fixed-size buffers (the paper I read that presented this in the context of MPI used linked lists, which clearly wouldn't work).

Another strategy that I used to improve the performance of my code was to use OpenCL-OpenGL interoperability to handle the data needed by both OpenCL and OpenGL by storing it in an OpenGL vertex buffer object (VBO) that is shared with OpenCL. This is extremely advantageous because after the data is initialized and sent to the GPU, the memory is never transferred back to the CPU, avoiding a potentially huge bottleneck. This was implemented from the very beginning, so I have no measure of the difference in performance.

Results

I tested the four kernels listed above with a wide variety of parameters to examine their performance. All of these tests were run on my desktop computer (even though we got OpenCL working on the Gates computers, my code was still running into other issues with them). Specs: EVGA GTX 560 Ti with 1 GB DDR5 RAM (specs specs2); AMD Phenom X4 9950 Black Edition (specs specs2); 8 GB DDR2 RAM; Ubuntu 13.04 with the nvidia 304 driver.

Before getting into details, here's an example of what a simulation looks like. The framerate is shown in the top left corner. Color is used primarily to judge depth. Since the camera can be rotated, color is varied in all dimensions. Nothing terribly exciting happens, just a simple demonstration.

Performance was measured based on the time (in ms) required to run kernel updates to force/position, averaged over 1 second intervals. The kernel calls and re-rendering the image were handled as two separate tasks, based on OpenGL's glutTimerFunc. Since the rendering is just a nice tool for us, we want to focus as much time as possible on running the kernel. In other words, the kernel is allowed to execute multiple times between updating the display. There is a minimum delay of 1ms between kernel calls and a minimum delay of 50ms between renders. So, just to be clear, I've used 'frame' to refer to a kernel update, not a render to the display (I should probably find a better word). It seems that times tend to cluster around certain data points, but they vary enough with all inputs to see some key information.

I focused of varying two of the parameters. Seven different values for the number of particles are used, ranging between 1024 and 16384. Seven different values are used for the size of a work group (a.k.a. size of a tile, where applicable), ranging between 16 and 1024. Some other important parameters are: bbox, the particles are constrained to $\pm bbox$ in all three dimensions and was set at 100 angstroms (with one exception); dt, the timestep was set to $10^{-15}$s (1 fs), which is reasonable for this type of simulation. The full data table can be found here. One way that I analyzed these was by plotting the results, grouping all with the same number of particles. One example is shown below, the rest can be found here. Each plot generally reflects the same trends, with some disagreement.

To me, the most striking result here is that ignoring far away particles makes a much greater difference than tiling does. My assumption was that the inherent divergence of this approach would drastically limit its effectiveness. However, the effects of divergence are still observed, given that performance for these generally peaks somewhere in the middle and goes down for the larger group sizes, as one might expect. Overall, the tiled approach generally shows a marginal advantage over the naive approach (when viewed holistically, as individual points vary considerably), but nothing to get too excited about. In the naive approach, there still is a fair amount of locality that can aid the calculation, even if it isn't explicitly designed around this.

Unfortunately, the results are very unclear with respect to what the best group size is. 64, 128, and 256 generally perform well, but there are exceptions. Since the natural SIMD width of the device is 32, it's interesting that larger groups are favored. This is likely again related to memory locality. With regard to the tiled approach, I would expect the best performance when roughly all positions for all concurrently executing tiles fit into the card's cache. I would need more information than I can find about the card specs to check this hypothesis though. This may be another reason that performance usually drops for the larger group sizes.

Code

For anyone who cares, the source code is available.

[github] [zip]

I can only guarantee it will compile and run on linux with an NVIDIA OpenCL device because that's all I've tried it on.

[PDF] [PPTX]

References

1. Steve Plimpton, Fast Parallel Algorithms for Short-Range Molecular Dynamics, Journal of Computational Physics, Volume 117, Issue 1, 1 March 1995, Pages 1-19, ISSN 0021-9991, 10.1006/jcph.1995.1039. (http://www.sciencedirect.com/science/article/pii/S002199918571039X)
2. Kevin J. Bowers, Edmond Chow, Huafeng Xu, Ron O. Dror, Michael P. Eastwood, Brent A. Gregersen, John L. Klepeis, Istvan Kolossvary, Mark A. Moraes, Federico D. Sacerdoti, John K. Salmon, Yibing Shan, and David E. Shaw. 2006. Scalable algorithms for molecular dynamics simulations on commodity clusters. In Proceedings of the 2006 ACM/IEEE conference on Supercomputing (SC '06). ACM, New York, NY, USA, , Article 84 . DOI=10.1145/1188455.1188544 http://sc06.supercomputing.org/schedule/pdf/pap259.pdf


text:
3 videos

3 videos

4 videos

3 videos

## Jean-Pierre Gazeau: "Illustration of Lie Group Theory with Real Matrices of Order Two"

00:00:00 / 00:00:00

## Large-scale machine learning and convex optimization 1/2

Many machine learning and signal processing problems are traditionally cast as convex optimization problems. A common difficulty in solving these problems is the size of the data, where there are many observations ("large n") and each of these is large ("large p"). In this setting, online algorithms such as stochastic gradient descent which pass over the data only once, are usually preferred over batch algorithms, which require multiple passes over the data. Given n observations/iterations, the optimal convergence rates of these algorithms are $O(1/\sqrt{n})$ for general convex functions and reaches $O(1/n)$ for strongly-convex functions. In this tutorial, I will first present the classical results in stochastic approximation and relate them to classical optimization and statistics results. I will then show how the smoothness of loss functions may be used to design novel algorithms with improved behavior, both in theory and practice: in the ideal infinite-data setting, an efficient novel Newton-based stochastic approximation algorithm leads to a convergence rate of $O(1/n)$ without strong convexity assumptions, while in the practical finite-data setting, an appropriate combination of batch and online algorithms leads to unexpected behaviors, such as a linear convergence rate for strongly convex problems, with an iteration cost similar to stochastic gradient descent.

### Citation data

• DOI 10.24350/CIRM.V.18919903
• Cite this video BACH Francis (2/2/16). Large-scale machine learning and convex optimization 1/2. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.18919903
• URL https://dx.doi.org/10.24350/CIRM.V.18919903

### Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

## Register

• Bookmark videos
• Add videos to see later &