text:
# Aerodynamic Parameter Estimation Using Flight Log Data

This example shows how to estimate plant dynamics of your UAV from flight log data.

### Overview

When using simulated models in unmanned aerial vehicle (UAV) design, you must develop a digital-twin plant model that is as close as possible to the physical behavior of your UAV. A digital twin is a simulation-based representation of the UAV. During the design phase, guidance, navigation, and control (GNC) engineers can utilize this digital twin to design their control and guidance algorithms. Developing an accurate digital-twin model is an iterative process that requires flight tests and resolving any discrepancies between the simulation and physical data. Developing a simulation model can be an expensive process, which can require extensive wind-tunnel testing or fluid dynamics analysis. This example shows how to estimate the plant model dynamics from flight log data that contains measured sensor data. The process consists of these steps:

1. Process the flight log.

2. Set up the physics model.

3. Estimate physics parameters.

4. Obtain physics model fitted to flight data.

### Visualize Flight Log and Identify Time of Interest

To visualize the flight log and identify a time of interest for parameter identification, use the flightLogAnalyzer function to open the Flight Log Analyzer app.

flightLogAnalyzer

On the app toolstrip, select Import and click From ULOG. Then, select quadrotor_model.ulg and click Open. Next, click Add Figure and, in the Plot section of the toolstrip, select the Height and IMU plots. In the figure pane, select the Height plot and, in the Signals pane, clear the Barometer Altitude and Estimated Altitude signals. Observe that significant activity originates at the 13.5 second mark in both the accelerometer and gyroscope readings. The GPS Altitude signal in the height plot indicates that the UAV has lifted off at the same time as this activity.

Define the start and end times for signal analysis based on this information.

tStart = 13.55;
tEnd = 68;

### Prepare Flight Log Data

For identifying the system, you must resample all flight log data to the same time steps. Select a sampling interval of 0.01 seconds. Next, call the helper function fetchSignalDataULog, which imports and resamples the data to the specified time range.

Import the flight log into the MATLAB® workspace.

ug = ulogreader("quadrotor_model.ulg"); % Copyright 2021 Manuel Yves Galliker and Autonomous Systems Lab ETH Zurich [1]

Resample the data to the new frequency to get timeseries data acc_x_T, acc_y_T, and acc_z_T for the x, y, and z readings of the accelerometer, respectively.

deltaT = 0.01;
tSample = tStart:deltaT:tEnd;
% Format Accelerometer, Gyroscope (output) and Actuator and Velocity (input) readings
[acc_x_T,acc_y_T,acc_z_T,ang_vel_T,actuatorOutput,velocityNED] = exampleHelperFetchSignalDataULog(ug,tSample);

Get the vehicle altitude from the flight data using the exampleHelperRawData helper function. Then, use the exampleHelperSlerpData helper function to interpolate the flight log orientation data using spherical interpolation to resample quaternion data at the new time steps.

vehicleAttitude = exampleHelperRawData(ug,"vehicle_attitude","q",1:4);
quatData = exampleHelperSlerpData(vehicleAttitude.Data,vehicleAttitude.Time,tSample);

To compute the resulting forces at each rotor, you must solve for the local airspeed in the body frame defined as:

${\mathit{V}}_{\mathrm{local}\text{\hspace{0.17em}}\mathrm{airspeed}}$=${\mathit{V}}_{\mathit{b}}+{\omega }_{\mathit{b}}×\mathit{R}$,

where:

• ${\mathit{V}}_{\mathit{b}}$ — Velocity of the body frame, derived from the velocity in the north-east-down (NED) reference frame,${\mathit{V}}_{\mathrm{NED}}$.

• ${\omega }_{\mathit{b}}$ — Angular velocity of the body frame.

• $\mathit{R}$ — 3D rotor position.

To do this, convert the groundspeed in the flight log to the body frame using orientation data for each time sample. Note that this conversion assumes wind velocity is zero, but you can add a wind correction if a wind estimate is available.

VNED = zeros(length(tSample),3);
Vb = zeros(length(tSample),3);
for ti = 1:1:length(tSample)
% Get velocity in NED frame at current time step
VNED(ti,1:3) = velocityNED.Data(ti,1:3);
% Calculate body velocity using orientation data and velocity in NED frame
Vb(ti,1:3) = quatrotate([quatData(ti,1) quatData(ti,2) quatData(ti,3) quatData(ti,4)],VNED(ti,1:3));
end

Convert the body velocity into the timeseries format.

Vb_T = timeseries(Vb,tSample);

Differentiate the angular x, y, and z velocity data from the gyroscope to get the angular acceleration measurements. Convert all the angular acceleration data into timeseries objects.

Set the actuator limits to the values actuator limits to a minimum value of 1000 and maximum value of 2000, to normalize the actuator inputs between 0 and 1.

n_Actuator_Inputs = normalizeActuators(actuatorOutput.Data,1000,2000);
n_Actuator_T = timeseries(n_Actuator_Inputs,tSample);

### Set Up Parameter Estimation Model

Open the data dictionary aeroParameters, and then open the plant model UAVQuadDynamics. The data dictionary contains aerodynamic parameters to use as inputs to the plant model.

open_system(simModel)

The plant model is set up in Simulink® as a dynamical model of quadrotor dynamics to get the predicted response of the system. The model takes airspeed, rotational velocity, and actuator inputs and outputs a predicted system response containing linear and angular accelerations.

Initialize the aerodynamic parameters with some estimates. See the Appendix section for more information about these aerodynamic parameters.

CD = 0.06;
CT1 = -0.05;
CT0 = 2;
CDFuselage = [0.025 0.025 0.025];
CM0 = 1.5;
CM1 = -0.01;
CDM0 = 0.15;
CDM1 = -0.04;
CRM = 0.01;

Open the Aerodynamic Parameters subsystem. The initialized aerodynamic parameters are inputs to the model in this subsystem.

### Estimate Plant Dynamics

Tune the aerodynamic parameters to match the predicted response of the Simulink model to the measured system response. You can use Simulink Design Optimization™ to automate this process. First, obtain parameter estimates using the Parameter Estimator app.

#### Create Parameter Estimation Script

Open the dynamics plant model UAVQuadDynamics with the Parameter Estimator app.

You can obtain the estimation setup by following the steps in this section, but if you want to skip to parameter estimation and tuning open the provided MAT file flightdata_spesession in the app and continue from the Tune Parameters section of this example.

From the app toolstrip, select New Experiment to open the Edit Experiment dialog box.

The first six fields in this box correspond to the six outputs of the dynamics plant model. Remove the Constant2 field by clicking the X icon for that row. Then, specify the corresponding time-series output signals for each of the remaining six fields. For example, specify the UAV/QuadDynamics/Plant_model:1 (acc_x) field as acc_x_T, which is the linear acceleration in the x-direction. Note that, after specifying a field, the value displays as <1x1 Signal, 5446 points>. These are the correspondences between the fields and the dynamics plant model outputs.

• acc_x field — acc_x_T output

• acc_y field — acc_y_T output

• acc_z field — acc_z_T output

• psi_x field — ang_acc_x_T output

• psi_y field — ang_acc_y_T output

• psi_z field — ang_acc_z_T output

Click Select Parameters and select these parameters:

• CD

• CD Fuselage

• CDM0

• CDM1

• CM0

• CM1

• CRM

• CT0

• CT1

Click OK to save your changes and close the Select mode variables dialog box. Click OK in the Edit Experiment dialog box.

Next, from the Parameter Estimator app toolstrip, click Estimate and select Generate MATLAB Function. The app generates a script to tune the parameters to the best values to fit to the flight log data.

#### Tune Parameters

Run the provided parameterEstimationUAVQuadDynamics script, which has been created using the same process as in the Create Parameter Estimation Script section, to automatically tune the parameters. Then update the parameters in the workspace.

% Tune the parameters
% Update the parameters in the workspace using the tuned parameters in pOpt
for i=1:1:length(pOpt)
eval(strcat(pOpt(i).Name,"=","[",num2str(pOpt(i).Value),"]"));
end

Note that the process of tuning the parameters can take some time. You can instead load the tuned parameters from the tunedParams MAT file.

### Evaluate Fit to Log Data

Simulate the plant model which now uses the tuned parameters.

### Starting serial model reference simulation build.
### Successfully updated the model reference simulation target for: RotorDragMoment
### Successfully updated the model reference simulation target for: ThrustForceModel

Build Summary

Simulation targets built:

Model             Action                        Rebuild Reason
=============================================================================================
RotorDragMoment   Code generated and compiled.  RotorDragMoment_msf.mexa64 does not exist.
ThrustForceModel  Code generated and compiled.  ThrustForceModel_msf.mexa64 does not exist.

2 of 2 models built (0 models already up to date)
Build duration: 0h 0m 32.128s
simOut =

tout: [5446x1 double]

ErrorMessage: [0x0 char]

Plot the x, y, and z acceleration output data from the model.

% X Acceleration Plot
figure
set(gcf,color="w")
hold on
plot(simOut.tout,simOut.yout{1}.Values.Data(:),LineWidth=2)
plot(acc_x_T)
title("Accelerometer X Data")
xlabel("Time (s)")
ylabel("Measurement (m/s^2)")
legend("Simulated","Flight Log")
hold off

% Y Acceleration Plot
figure
set(gcf,color="w")
hold on
plot(simOut.tout,simOut.yout{2}.Values.Data(:),LineWidth=2)
plot(acc_y_T)
title("Accelerometer Y Data")
xlabel("Time (s)")
ylabel("Measurement (m/s^2)")
legend("Simulated","Flight Log")
hold off

% Z Acceleration Plot
figure
set(gcf,color="w")
hold on
plot(simOut.tout,simOut.yout{3}.Values.Data(:),LineWidth=2)
plot(acc_z_T)
title("Accelerometer Z Data")
xlabel("Time (s)")
ylabel("Measurement (m/s^2)")
legend("Simulated","Flight Log")
hold off

Calculate the root mean square error (RMSE) between the x-, y-, and z-data in the plant model and the x-, y-, and z-measurements in the flight log.

RMSE_Acc_X = sqrt(mean((acc_x_T.Data-simOut.yout{1}.Values.Data(:)).^2))
RMSE_Acc_X = 0.0314
RMSE_Acc_Y = sqrt(mean((acc_y_T.Data-simOut.yout{2}.Values.Data(:)).^2))
RMSE_Acc_Y = 0.0431
RMSE_Acc_Z = sqrt(mean((acc_z_T.Data-simOut.yout{3}.Values.Data(:)).^2))
RMSE_Acc_Z = 0.1975

The RMSE is low, which indicates that the tuned parameters fit the flight log well.

Discard the changes to the plant data dictionary and close the model.

close_system(simModel,0)

### Summary

The estimated dynamics plant model fits the response of the given flight log data. As a next step, you can design a controller to control the obtained plant model dynamics. Also, because the current workflow uses readings obtained from derivatives of raw gyroscope data, you can better estimate angular acceleration dynamics by adding a filter to smooth the gyroscope data prior to identification. You can also utilize more flight logs to further refine your estimate of the plant dynamics.

### Appendix

This section contains a brief summary of the mathematical model used to estimate quadrotor dynamics. For a detailed study, see [1].

You can compute the predicted moment forces based on the state of the quadrotor at any timestep. These predictions depend on the aerodynamic parameters ${\mathit{C}}_{\mathrm{T0}}$, ${\mathit{C}}_{\mathrm{T1}}$, ${\mathit{C}}_{\mathit{D}}$, ${\mathit{C}}_{\mathrm{DM0}}$, ${\mathit{C}}_{\mathrm{DM1}}$, ${\mathit{C}}_{\mathrm{Dx}}$, ${\mathit{C}}_{\mathrm{Dy}}$, ${\mathit{C}}_{\mathrm{Dz}}$,${\mathit{C}}_{\mathrm{M0}}$, ${\mathit{C}}_{\mathrm{M1}}$, and ${\mathit{C}}_{\mathrm{RM}}\text{\hspace{0.17em}}$. The measured linear and angular acceleration are:

${\mathit{a}}_{\mathrm{meas}}=\left(\frac{{\mathit{F}}_{\mathit{b}}^{\mathrm{total}}}{\mathit{m}}\right)$, and

${\Psi }_{\mathrm{meas}}$=${\mathit{I}}^{-1}$(${\mathit{M}}_{\mathit{b}}^{\mathrm{total}}$-${\omega }_{\mathit{b}}$x$\mathit{I}$${\omega }_{\mathit{b}}$)

where:

${\mathit{a}}_{\mathrm{meas}}$ — Measured linear acceleration.

${\Psi }_{\mathrm{meas}}$ — Measured angular acceleration.

$\mathit{I}$— Moment of inertia of the UAV body.

${\omega }_{\mathit{b}}$ — Angular velocity in the body frame.

${\mathit{F}}_{\mathit{b}}^{\mathrm{total}}$ — Predicted force in the body frame.

${\mathit{M}}_{\mathit{b}}^{\mathrm{total}}$ — Predicted moment in the body frame.

${\omega }_{\mathit{b}}$ — Angular velocity in the body frame.

#### Force Computation

These are the contributions of forces. In this section, ${\mathit{v}}_{\mathit{l}}$ and ${\mathit{v}}_{\mathit{p}}$ are the parallel and perpendicular velocity components at each rotor, and ${\mathit{p}}_{\mathrm{rotor}}$ is the outward normal from the rotor.

The advance ratio at each rotor is:

$\mathit{J}=\frac{{\mathit{v}}_{\mathit{l}}}{\eta \mathit{D}}$

The thrust of each rotor is:

${\mathit{F}}_{\mathit{T}}^{\mathit{b}}$=$\rho {\eta }^{2}{\mathit{D}}^{4}$(${\mathit{C}}_{\mathrm{T0}}$+${\mathit{C}}_{\mathrm{T1}}\mathit{J}\right){\mathit{p}}_{\mathrm{rotor}}$

The rotor drag is:

${\mathit{F}}_{\mathit{D}}^{\mathit{b}}$=${-\mathit{C}}_{\mathit{D}}$$\eta$${\mathit{v}}_{\mathit{p}}$

The area of the fuselage is included in the drag coefficient. The fuselage drag in the x-, y-, and z-directions is:

${\mathit{F}}_{\mathrm{DFuselage}\text{\hspace{0.17em}}\mathit{x}|\mathit{y}|\mathit{z}}^{\mathit{b}}$|=-0.5*${\mathit{C}}_{\mathrm{Dx}|\mathit{y}|\mathit{z}}\rho {\mathit{V}}_{\mathit{x},\mathit{y},\mathit{z}}$$|{\mathit{V}}_{\mathit{x},\mathit{y},\mathit{z}}|$

#### Moment Computation

The model is also parameterized for moment contribution.

The moment contribution of thrust is:

${\mathit{M}}_{\mathit{T}}^{\mathit{b}}$=${\mathit{R}}_{\mathrm{arm}}\otimes \rho {\eta }^{2}{\mathit{D}}^{4}$(${\mathit{C}}_{\mathrm{M0}}$+${\mathit{C}}_{\mathrm{M1}}\mathit{J}\right){\mathit{p}}_{\mathrm{rotor}}$.

The rotor drag moment is:

${\mathit{M}}_{\mathit{D}}^{\mathit{b}}$=$\rho {\eta }^{2}{\mathit{D}}^{5}\left({\mathit{C}}_{\mathrm{Dm0}}+{\mathit{C}}_{\mathrm{Dm1}}\mathit{J}\right)$${\mathit{p}}_{\mathrm{rotor}}$.

The rotor rolling moment is:

${\mathit{M}}_{\mathit{R}}^{\mathit{b}}$=-${\mathit{C}}_{\mathrm{RM}}$$\eta$(TurnDir.${\mathit{p}}_{\mathrm{rotor}}$)${\mathit{v}}_{\mathit{p}}$.

You can obtain the linear acceleration measurement directly from accelerometer readings in the flight log, but there is no direct signal measuring angular acceleration in the flight log (${\Psi }_{\mathrm{meas}}$). Thus, you can use a time derivative of the gyroscope readings to obtain this measurement.

${\Psi }_{\mathrm{meas}}$=$\frac{\mathit{d}{\omega }_{\mathit{b}}}{\mathrm{dt}}$

Alternatively, if a separate measurement of angular acceleration is available, you can use that as a source for parameter estimation.

You can use the first two equations for ${\mathit{a}}_{\mathrm{meas}}$ and ${\Psi }_{\mathrm{meas}}$ to compute the predicted accelerations and angular momentum based on a parameterized Simulink model, and optimize the fit to the measured angular and linear acceleration.

### References

[1] Galliker, Manuel Yves. "Data-Driven Dynamics Modelling Using Flight Logs." June 24, 2021. https://doi.org/10.3929/ETHZ-B-000507495.

Copyright 2022 The MathWorks, Inc.


text:
Accelerating the pace of engineering and science

# Fixed Orifice Empirical

Fixed hydraulic orifice based on empirical data

Orifices

## Description

The Fixed Orifice Empirical block models a fixed orifice in hydraulic systems with data obtained from experimental testing. The data required for characterization is the set of pressure differentials across the orifice, together with associated flow rates determined for a particular fluid and temperature.

The flow rate through the orifice is determined with the table lookup block from the set of experimental measurements

q = f(p)

where

 q Volumetric flow rate p Pressure differential

You can select from three interpolation and two extrapolation methods.

 Note   Extrapolation could result in large errors if the operating point deviates significantly from the area of experiments.

The block positive direction is from port A to port B. This means that the flow rate is positive if it flows from A to B, and the pressure differential is determined as $p={p}_{A}-{p}_{B}$.

## Dialog Box and Parameters

Tabulated pressure differentials

Specify the pressure differential vector as a one-dimensional array. The vector contains values of pressure differentials obtained during experimental characterization of the orifice. The vector must be strictly increasing. The values can be nonuniformly spaced. The minimum number of values depends on the interpolation method: you must provide at least two values for linear interpolation, at least three values for cubic or spline interpolation. The default values, in Pa, are [ -4e+6 -3e+6 -2e+6 -1e+6 -5e+5 0 5e+5 1e+6 2e+6 3e+6 4e+6 ].

Tabulated flow rates

Specify the vector of flow rates through the orifice, corresponding to these pressure differentials, as a one-dimensional array. The vector must be of the same size as the Tabulated pressure differentials vector. The default values, in m^3/s, are [ -0.0024436 -0.0021248 -0.0016852 -0.0012248 -8.4476e-4 0 8.5333e-4 0.0012068 0.0017067 0.0020902 0.0024136 ].

Interpolation method

Select one of the following interpolation methods for approximating the output value when the input value is between two consecutive grid points:

• Linear — Uses a linear interpolation function.

• Cubic — Uses the Piecewise Cubic Hermite Interpolation Polinomial (PCHIP).

• Spline — Uses the cubic spline interpolation algorithm.

For more information on interpolation algorithms, see the PS Lookup Table (1D) block reference page.

Extrapolation method

Use extrapolation with extreme caution, because moving beyond the measurement limits could result in large errors. Select one of the following extrapolation methods for determining the output value when the input value is outside the range specified in the argument list:

• From last 2 points — Extrapolates using the linear method (regardless of the interpolation method specified), based on the last two output values at the appropriate end of the range. That is, the block uses the first and second specified output values if the input value is below the specified range, and the two last specified output values if the input value is above the specified range.

• From last point — Uses the last specified output value at the appropriate end of the range. That is, the block uses the last specified output value for all input values greater than the last specified input argument, and the first specified output value for all input values less than the first specified input argument.

For more information on extrapolation algorithms, see the PS Lookup Table (1D) block reference page.

## Ports

The block has the following ports:

A

Hydraulic conserving port associated with the orifice inlet.

B

Hydraulic conserving port associated with the orifice outlet.

format: plain


text:
## 6. The Birthday Problem

### Introduction

#### The Sampling Model

As in the basic sampling model, suppose that we select $$n$$ numbers at random, with replacement, from the population $$D =\{1, 2, \ldots, m\}$$. Thus, our outcome vector is $$\bs{X} = (X_1, X_2, \ldots, X_n)$$ where $$X_i$$ is the $$i$$th number chosen. Recall that our basic modeling assumption is that $$\bs{X}$$ is uniformly distributed on the sample space $$S = D^n = \{1, 2, \ldots, m\}^n$$

In this section, we are interested in the number of population values missing from the sample, and the number of (distinct) population values in the sample. The computation of probabilities related to these random variables are generally referred to as birthday problems. Often, we will interpret the sampling experiment as a distribution of $$n$$ balls into $$m$$ cells; $$X_i$$ is the cell number of ball $$i$$. In this interpretation, our interest is in the number of empty cells and the number of occupied cells.

For $$i \in D$$, let $$Y_i$$ denote the number of times that $$i$$ occurs in the sample: $Y_i = \#\left\{j \in \{1, 2, \ldots, n\}: X_j = i\right\} = \sum_{j=1}^n \bs{1}(X_j = i)$

$$\bs{Y} = (Y_1, Y_2, \ldots, Y_m)$$ has the multinomial distribution with parameters $$n$$ and $$(1/m, 1/m, \ldots, 1/m)$$: $\P(Y_1 = y_1, Y_2 = y_2, \ldots, Y_m = y_m) = \binom{n}{y_1, y_2, \ldots, y_n} \frac{1}{m^n}, \quad (y_1, y_2, \ldots, y_m) \in \N^n \text{ with } \sum_{i=1}^m y_i = n$

Proof:

This follows immediately from the definition of the multinomial distribution, since $$(X_1, X_2, \ldots, X_n)$$ is an independent sequence, and $$X_i$$ is uniformly distributed on $$\{1, 2, \ldots, m\}$$ for each $$i$$.

We will now define the main random variables of interest.

The number of population values missing in the sample is $U = \#\left\{j \in \{1, 2, \ldots, m\}: Y_j = 0\right\} = \sum_{j=1}^m \bs{1}(Y_j = 0)$ and the number of (distinct) population values that occur in the sample is $V = \#\left\{j \in \{1, 2, \ldots, m\}: Y_j \gt 0\right\} = \sum_{j=1}^m \bs{1}(Y_j \gt 0)$ Also, $$U$$ takes values in $$\{\max\{m - n, 0\}, \ldots, m - 1\}$$ and $$V$$ takes values in $$\{1, 2, \ldots, \min\{m,n\}\}$$.

Clearly we must have $$U + V = m$$ so once we have the probability distribution and moments of one variable, we can easily find them for the other variable. However, we will first solve the simplest version of the birthday problem.

### The Simple Birthday Problem

The event that there is at least one duplication when a sample of size $$n$$ is chosen from a population of size $$m$$ is $B_{m,n} = \{V \lt n\} = \{U \gt m - n\}$ The (simple) birthday problem is to compute the probability of this event. For example, suppose that we choose $$n$$ people at random and note their birthdays. If we ignore leap years and assume that birthdays are uniformly distributed throughout the year, then our sampling model applies with $$m = 365$$. In this setting, the birthday problem is to compute the probability that at least two people have the same birthday (this special case is the origin of the name).

The solution of the birthday problem is an easy exercise in combinatorial probability.

The probability of the birthday event is $\P\left(B_{m,n}\right) = 1 - \frac{m^{(n)}}{m^n}, \quad n \le m$ and $$P\left(B_{m,n}\right) = 1$$ for $$n \gt m$$

Proof:

The complementary event $$B^c$$ occurs if and only if the outcome vector $$\bs{X}$$ forms a permutation of size $$n$$ from $$\{1, 2, \ldots, m\}$$. The number of permutations is $$m^{(n)}$$ and of course the number of samples is $$m^n$$.

The fact that the probability is 1 for $$n \gt m$$ is sometimes referred to as the pigeonhole principle: if more than $$m$$ pigeons are placed into $$m$$ holes then at least one hole has 2 or more pigeons. The following result gives a recurrence relation for the probability of distinct sample values and thus gives another way to compute the birthday probability.

Let $$p_{m,n}$$ denote the probability of the complementary birthday event $$B^c$$, that the sample variables are distinct, with population size $$m$$ and sample size $$n$$. Then $$p_{m,n}$$ satisfies the following recursion relation and initial condition:

1. $$p_{m,n+1} = \frac{m-n}{m} p_{m,n}$$
2. $$p_{m,1} = 1$$

#### Examples

Let $$m = 365$$ (the standard birthday problem).

1. $$\P\left(B_{365,10}\right) = 0.117$$
2. $$\P\left(B_{365,20}\right) = 0.411$$
3. $$\P\left(B_{365,30}\right) = 0.706$$
4. $$\P\left(B_{365,40}\right) = 0.891$$
5. $$\P\left(B_{365,50}\right) = 0.970$$
6. $$\P\left(B_{365,60}\right) = 0.994$$

In the birthday experiment, set $$n = 365$$ and select the indicator variable $$I$$. For $$n \in \{10, 20, 30, 40, 50, 60\}$$ run the experiment 1000 times each and compare the relative frequencies with the true probabilities.

In spite of its easy solution, the birthday problem is famous because, numerically, the probabilities can be a bit surprising. Note that with a just 60 people, the event is almost certain! Mathematically, the rapid increase in the birthday probability, as $$n$$ increases, is due to the fact that $$m^n$$ grows much faster than $$m^{(n)}$$.

Four fair, standard dice are rolled. Find the probability that the scores are distinct.

$$\frac{5}{18}$$

In the birthday experiment, set $$m = 6$$ and select the indicator variable $$I$$. Vary $$n$$ with the scrollbar and note graphically how the probabilities change. Now with $$n = 4$$, run the experiment 1000 times and compare the relative frequency of the event to the corresponding probability.

Five persons are chosen at random.

1. Find the probability that at least 2 have the same birth month.
2. Criticize the sampling model in this setting

$$\frac{89}{144}$$

In the birthday experiment, set $$m = 12$$ and select the indicator variable $$I$$. Vary $$n$$ with the scrollbar and note graphically how the probabilities change. Now with $$n = 5$$, run the experiment 1000 times and compare the relative frequency of the event to the corresponding probability.

A fast-food restaurant gives away one of 10 different toys with the purchase of a kid's meal. A family with 5 children buys 5 kid's meals. Find the probability that the 5 toys are different.

$$\frac{189}{625}$$

In the birthday experiment, set $$m = 10$$ and select the indicator variable $$I$$. Vary $$n$$ with the scrollbar and note graphically how the probabilities change. Now with $$n = 5$$, run the experiment 1000 times and comparethe relative frequency of the event to the corresponding probability.

Let $$m = 52$$. Find the smallest value of $$n$$ such that the probability of a duplication is at least $$\frac{1}{2}$$.

Summary:

$$n = 9$$

### The General Birthday Problem

We now return to the more general problem of finding the distribution of the number of distinct sample values and the distribution of the number of excluded sample values.

#### The Probability Density Function

The number of samples with exactly $$j$$ values excluded is $\#\{U = j\} = \binom{m}{j} \sum_{k=0}^{m-j} (-1)^k \binom{m - j}{k}(m - j - k)^n, \quad j \in \{\max\{m-n, 0\}, \ldots, m - 1\}$

Proof:

For $$i \in D$$, consider the event that $$i$$ does not occur in the sample: $$A_i = \{Y_i = 0\}$$. Now let $$K \subseteq D$$ with $$\#(K) = k$$. Using the multiplication rule of combinatorics, it is easy to count the number of samples that do not contain any elements of $$K$$: $\#\left(\bigcap_{i \in K} A_i\right) = (m - k)^n$ Now the inclusion-exclusion rule of combinatorics can be used to count the number samples that are missing at least one population value: $\#\left(\bigcup_{i=1}^m A_i\right) = \sum_{k=1}^m (-1)^{k-1} \binom{m}{k}(m - k)^n$ Once we have this, we can use DeMorgan's law to count the number samples that contain all population values: $\#\left(\bigcap_{i=1}^m A_i^c\right) = \sum_{k=0}^m (-1)^k \binom{m}{k} (m - k)^n$ Now we can use a two-step procedure to generate all samples that exclude exactly $$j$$ population values: First, choose the $$j$$ values that are to be excluded. The number of ways to perform this step is $$\binom{m}{j}$$. Next select a sample of size $$n$$ from the remaining population values so that none are excluded. The number of ways to perform this step is the result in the last displayed equation, but with $$m - j$$ replacing $$m$$. The multiplication principle of combinatorics gives the result.

The distributions of the number of excluded values and the number of distinct values are now easy.

The probability density function of $$U$$ is given by $\P(U = j) = \binom{m}{j} \sum_{k=0}^{m-j} (-1)^k \binom{m-j}{k}\left(1 - \frac{j + k}{m}\right)^n, \quad j \in \{\max\{m-n,0\}, \ldots, m-1\}$

Proof:

Since the samples are uniformly distributed, $$\P(U = j) = \#\{U = j\} / m^n$$ and so the result follows from the previous exercise.

The probability density function of the number of distinct values $$V$$ is given by $\P(V = j) = \binom{m}{j} \sum_{k=0}^j (-1)^k \binom{j}{k} \left(\frac{j - k}{m}\right)^n, \quad j \in \{1, 2, \ldots, \min\{m,n\}\}$

Proof:

This follows from the previous theorem since $$\P(V = j) = \P(U = m - j).$$

In the birthday experiment, select the number of distinct sample values. Vary the parameters and note the shape and location of the probability density function. For selected values of the parameters, run the simulation 1000 and compare the relative frequency function to the probability density function.

The distribution of the number of excluded values can also be obtained by a recursion argument.

Let $$f_{m,n}$$ denote the probability density function of the number of excluded values $$U$$, when the population size is $$m$$ and the sample size is $$n$$. Then

1. $$f_{m,1}(m - 1) = 1$$
2. $$f_{m,n+1}(j) = \frac{m - j}{m} f_{m,n}(j) + \frac{j+1}{m} f_{m,n}(j+1)$$

#### Moments

Now we will find the means and variances. The number of excluded values and the number of distinct values are counting variables and hence can be written as sums of indicator variables. As we have seen in many other models, this representation is frequently the best for computing moments.

For $$j \in \{0, 1, \ldots, m\}$$, let $$I_j = \bs{1}(Y_j = 0)$$, the indicator variable of the event that $$j$$ is not in the sample. Note that the number of population values missing in the sample can be written as the sum of the indicator variables: $U = \sum_{j=1}^m I_j$

For distinct $$i, \, j \in \{1, 2, \ldots, m\}$$,

1. $$E\left(I_j\right) = \left(1 - \frac{1}{m}\right)^n$$
2. $$\var\left(I_j\right) = \left(1 - \frac{1}{m}\right)^n - \left(1 - \frac{1}{m}\right)^{2\,n}$$
3. $$\cov\left(I_i, I_j\right) = \left(1 - \frac{2}{m}\right)^n - \left(1 - \frac{1}{m}\right)^{2\,n}$$
Proof:

Since each population value is equally likely to be chosen, $$\P(I_j = 1) = (1 - 1 / m)^n$$. Thus, parts (a) and (b) follow from standard results for the mean and variance of an indicator variable. Next, $$I_i I_j$$ is the indicator variable of the event that $$i$$ and $$j$$ are both excluded, so $$\P(I_i I_j = 1) = (1 - 2 / m)^n$$. Part (c) then follows from the standard formula for covariance.

The expected number of excluded values and the expected number of distinct values are

1. $$\E(U) = m \left(1 - \frac{1}{m}\right)^n$$
2. $$\E(V) = m \left[1 - \left(1 - \frac{1}{m}\right)^n \right]$$
Proof:

Part (a) follows from the previous exericse and the representation $$U = \sum_{j=1}^n I_j$$. Part (b) follows from part (a) since $$U + V = m$$.

The variance of the number of exluded values and the variance of the number of distinct values are $\var(U) = \var(V) = m (m - 1) \left(1 - \frac{2}{m}\right)^n + m \left(1 - \frac{1}{m}\right)^n - m^2 \left(1 - \frac{1}{m}\right)^{2 n}$

Proof:

Recall that $$\var(U) = \sum_{i=1}^m \sum_{j=1}^m \cov(I_i, I_j)$$. Using the results above on the covariance of the indicator variables and simplifying gives the variance of $$U$$. Also, $$\var(V) = \var(U)$$ since $$U + V = m$$.

In the birthday experiment, select the number of distinct sample values. Vary the parameters and note the size and location of the mean $$\pm$$ standard-deviation bar. For selected values of the parameters, run the simulation 1000 times and compare the sample mean and variance to the distribution mean and variance.

#### Examples and Applications

Suppose that 30 persons are chosen at random. Find each of the following:

1. The probability density function of the number of distinct birthdays.
2. The mean of the number of distinct birthdays.
3. The variance of the number of distinct birthdays.
4. The probability that there are at least 28 different birthdays represented.
1. $$\P(V = j) = \binom{30}{j} \sum_{k=0}^j (-1)^k \left(\frac{j-k}{365}\right)^{30}, \quad j \in \{1, 2, \ldots, 30\}$$
2. $$\E(V) = 28.8381$$
3. $$\var(V) = 1.0458$$
4. $$\P(V \ge 28) = 0.89767$$

In the birthday experiment, set $$m = 365$$ and $$n = 30$$. Run the experiment 1000 times with an update frequency of 10 and compute the relative frequency of the event in part (d) of the last exercise.

Suppose that 10 fair dice are rolled. Find each of the following:

1. The probability density function of the number of distinct scores.
2. The mean of the number of distinct scores.
3. The variance of the number of distinct scores.
4. The probability that there will 4 or fewer distinct scores.
1. $$\P(V = j) = \binom{10}{j} \sum_{k=0}^j (-1)^k \binom{j}{k} \left(\frac{j-k}{6}\right)^{10}, \quad j \in \{1, 2, \ldots, 6\}$$
2. $$\E(V) = 5.0310$$
3. $$\var(V) = 0.5503$$
4. $$\P(V \le 4) = 0.22182$$

In the birthday experiment, set $$m = 6$$ and $$n = 10$$. Run the experiment 1000 times and compute the relative frequency of the event in part (d) of the last exercise.

A fast food restaurant gives away one of 10 different toys with the purchase of each kid's meal. A family buys 15 kid's meals. Find each of the following:

1. The probability density function of the number of toys that are missing.
2. The mean of the number of toys that are missing.
3. The variance of the number of toys that are missing.
4. The probability that at least 3 toys are missing.
Answwer:
1. $$\P(U = j) = \binom{15}{j} \sum_{k=0}^{10-j} (-1)^k \binom{10-j}{k}\left(1 - \frac{j+k}{10}\right)^{15}, \quad j \in \{0, 1, \ldots, 9\}$$
2. $$\E(U) = 2.0589$$
3. $$\var(U) = 0.9864$$
4. $$\P(U \ge 3) = 0.3174$$

In the birthday experiment, set $$m = 10$$ and $$n = 15$$. Run the experiment 1000 times and compute the relative frequency of the event in part (d).

The lying students problem. Suppose that 3 students, who ride together, miss a mathematics exam. They decide to lie to the instructor by saying that the car had a flat tire. The instructor separates the students and asks each of them which tire was flat. The students, who did not anticipate this, select their answers independently and at random. Find each of the following:

1. The probability density function of the number of distinct answers.
2. The probability that the students get away with their deception.
3. The mean of the number of distinct answers.
4. The standard deviation of the number of distinct answers.
1.  $$j$$ $$\P(V = j)$$ 1 2 3 $$\frac{1}{16}$$ $$\frac{9}{16}$$ $$\frac{6}{16}$$
2. $$\P(V = 1) = \frac{1}{16}$$
3. $$\E(V) = \frac{37}{16}$$
4. $$\sd(V) = \sqrt{\frac{87}{256}} \approx 0.58296$$

The duck hunter problem. Suppose that there are 5 duck hunters, each a perfect shot. A flock of 10 ducks fly over, and each hunter selects one duck at random and shoots. Find each of the following:

1. The probability density function of the number of ducks that are killed.
2. The mean of the number of ducks that are killed.
3. The standard deviation of the number of ducks that are killed.
1.  $$j$$ $$\P(V = j)$$ 1 2 3 4 5 $$\frac{1}{10\,000}$$ $$\frac{27}{2000}$$ $$\frac{9}{50}$$ $$\frac{63}{125}$$ $$\frac{189}{625}$$
2. $$\E(V) = \frac{40\,951}{10\,000} = 4.0951$$
3. $$\sd(V) = 0.72768$$


text:
# Chain rule in $\mathbb{R}^n$, did I wrote it down correctly?

everyone. I had to use the chain rule and I am a bit confused by the notation, could you please tell me if I wrote it down correctly ?

I have a map $$H : \mathbb{R}^{2n} \rightarrow \mathbb{R}$$ and I take two smooth periodic functions $$x,y \in C^{\infty}(S^1,\mathbb{R}^{2n})$$, i.e. $$x(t),y(t) \in \mathbb{R}^{2n}$$.

Now I have to evaluate

$$\frac{d}{d \epsilon} \mid_{\epsilon = 0} \int_0^1 H(x+\epsilon y) dt$$.

Here's my attempt

$$H(x+\epsilon y)=H(z_1,...,z_{2n})$$ and hence

$$\frac{d}{d \epsilon} \mid_{\epsilon = 0} \int_0^1 H(z_1,...,z_{2n}) dt = \int_0^1 \sum_{i=1}^{2n} \frac{\partial H}{\partial z_i} \frac{d z_i}{d \epsilon} \mid_{\epsilon =0} dt= \int_0^1 < \nabla H(x),y> dt$$

• Looks right to me – Daniel Gendin Mar 4 at 22:34
• Thanks :) I'm sometimes a bit confused with the notation for the chain rule. – Alain Mar 5 at 10:32


text:
# What is the slope of the line normal to the tangent line of f(x) = xcotx+2xsin(x-pi/3)  at  x= (15pi)/8 ?

Aug 12, 2017

$- \frac{2}{15 \sqrt{3} \pi + 4}$

#### Explanation:

$\Rightarrow x \cot x + 2 x \sin \left(x - \frac{\pi}{3}\right)$

For reference :-
$\sin \left(\frac{15 \pi}{8}\right) = \frac{1}{2}$
$\cos \left(\frac{15 \pi}{8}\right) = - \frac{\sqrt{3}}{2}$
$\cos e c \left(\frac{15 \pi}{8}\right) = 2$
$\cot \left(\frac{15 \pi}{8}\right) = - \sqrt{3}$

As slope of any line is the derivative of the equation, I will differentiate the equation of tangent.

$\Rightarrow \frac{\mathrm{dy}}{\mathrm{dx}} = - x \cos e {c}^{2} x \cot x + 2 \left[\sin \left(x - \frac{\pi}{3}\right) + \cos \left(x - \frac{\pi}{3}\right)\right]$

clearly,
Here I can see the trigonometric formula of $\sin \left(A - B\right) \mathmr{and} \cos \left(A - B\right)$
Solving,
$\sin \left(x - \frac{\pi}{3}\right) + \cos \left(x - \frac{\pi}{3}\right)$
by above 2 formulas, I get,
$\left(\sin x + \cos x\right) + \sqrt{3} \left(\sin x - \cos x\right)$

So, at $x = \frac{15 \pi}{8}$,
The value of above equation becomes $2$

Now, at $x = \frac{15 \pi}{8}$,
$\frac{\mathrm{dy}}{\mathrm{dx}} = \frac{15 \sqrt{3} \pi + 4}{2} = {m}_{\text{1}}$

Now, when a line is normal to the tangent line, it means that the line is perpendicular to the tangent line.

Let the slope of perpendicular line be ${m}_{\text{2}}$

If the lines are perpendicular to each other then,
${m}_{\text{1"m_"2}} = - 1$

So, using above equation the slope of line normal to the tangent comes out to be,

${m}_{\text{2}} = - \frac{2}{15 \sqrt{3} \pi + 4}$

ENJOY MATHS !!!!!!!!


text:
## Stream: new members

### Topic: semialgebra setminus

#### Iocta (Mar 16 2021 at 20:27):

What's wrong here?

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra (α : Type*) :=
(semialgebra' : set (set α) → Prop)
(semialgebra_empty : semialgebra' ∅)
(semialgebra_inter : ∀ (s : set (set α)) (hs : semialgebra' s) (s1 s2 : set α), s1 ∈ s → s2 ∈ s → (s1 ∩ s2) ∈ s)
(semialgebra_difference : ∀ (s t : set (set α)), ∃ c : finset (set α), (finset.bUnion c) = s \ t)

-- type mismatch at application
--   has_sdiff.sdiff s
-- term
--   s
-- has type
--   set (set α) : Type ?
-- but is expected to have type
--   (set α → finset ?m_1) → finset ?m_1 : Type (max ? ?)

#### Alex J. Best (Mar 16 2021 at 20:45):

I think your definition has too many levels of nested sets, set X is the power set set (set X) is subsets of the power set but set (set X)) \to Prop is another condition on those, so a further power set.

import data.finset.basic

open set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_difference : ∀ (s t : set α), in_semialgebra s → in_semialgebra t → ∃ c : finset (set α), ∀ s' ∈ c, in_semialgebra s' → (sUnion (c : set (set α))) = s \ t)

looks more like what I read on https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras if that's what youre trying.

#### Alex J. Best (Mar 16 2021 at 20:45):

I had to cast the finset to a set to take the set docs#set.sUnion and also deleted the repeated introduction of alpha.

#### Alex J. Best (Mar 16 2021 at 20:52):

I guess that page also includes a pairwise disjoint condition which is missing from what I wrote

#### Iocta (Mar 16 2021 at 21:05):

I see. That in_ naming scheme is very clarifying. I was confused thinking the first component's argument was the semialgebra instead of a member of it.

#### Iocta (Mar 16 2021 at 22:06):

is the "disjoint" condition actually doing any work or can I just delete it?

#### Iocta (Mar 16 2021 at 22:07):

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

#### Iocta (Mar 16 2021 at 22:13):

(Also, why is that definition so different from the one on wikibooks)

#### Iocta (Mar 17 2021 at 22:46):

I thought it was gonna ask me to show that empty is in I, but it's asking for nullset equals I. I guess I've made the same mistake again, but I don't see how.

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example (I : {s : set ℝ // ∃ (a b : ℝ), s = Icc a b}) : semialgebra I := {
in_semialgebra := heq I,
semialgebra_empty := _,
semialgebra_inter := _,
semialgebra_compl := _
}

-- don't know how to synthesize placeholder
-- context:
-- I : {s // ∃ (a b : ℝ), s = Icc a b}
-- ⊢ I == ∅

#### Eric Wieser (Mar 17 2021 at 22:59):

Are you sure you want heq I as your in_semi_algebra?

#### Eric Wieser (Mar 17 2021 at 22:59):

It's very rare to want docs#heq unless you're really running into dependently-typed trouble

#### Eric Wieser (Mar 17 2021 at 23:01):

Is it possible you wanted this?

example : semialgebra ℝ := {
-- the semialgebra contains closed intervals of ℝ
in_semialgebra := λ s, ∃ (a b : ℝ), s = Icc a b,
semialgebra_empty := ⟨0, 0, sorry⟩,
semialgebra_inter := sorry,
semialgebra_compl := sorry
}

#### Iocta (Mar 17 2021 at 23:03):

That looks more right, I'll try that

#### Iocta (Mar 17 2021 at 23:05):

I guess that's actually asking me to show $[0,0] = \emptyset$ which probably isn't true. So maybe my statement of the problem is broken in the first place.

#### Eric Wieser (Mar 17 2021 at 23:51):

Oh yeah, I forgot what closed meant!

#### Iocta (Mar 18 2021 at 19:36):

What is this error?

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example : semialgebra ℝ := {
in_semialgebra := λ s, s = ∅ ∨ ∃ (a b : ℝ),  (a < b → s = (Ioc a b)),
semialgebra_empty := or.inl rfl,
semialgebra_inter := begin
intros s1 s2 h1 h2,
cases h1 with h1 h1,
{
cases h2 with h2 h2,
{
left,
rw [h1, empty_inter],
},
{
left,
rw [h1, empty_inter],
},
},
{
cases h2,
{
left,
rw [h2, inter_empty],
},
{
right,
cases h1 with a1 h1,
cases h1 with b1 h1,
rw h1,
cases h2 with a2 h2,
cases h2 with b2 h2,
rw h2,
{
use a1 ⊔ a2,
use b1 ⊓ b2,
intro h,
rw Ioc_inter_Ioc,
},
{
apply (classical.em (a2 < b2)),
-- invalid apply tactic, failed to unify
--   a2 < b2
-- with
--   a2 < b2 ∨ ¬a2 < b2
-- state:
-- s1 s2 : set ℝ,
-- a1 b1 : ℝ,
-- h1 : a1 < b1 → s1 = Ioc a1 b1,
-- a2 b2 : ℝ,
-- h2 : a2 < b2 → s2 = Ioc a2 b2
-- ⊢ a2 < b2
},
{
sorry,
},
},
}
end,
semialgebra_compl := begin
sorry
end
}

#### Kevin Buzzard (Mar 18 2021 at 19:37):

Do you understand what the apply tactic does? It changes a goal of the form Q to a goal of the form P if you apply f : P -> Q.

#### Kevin Buzzard (Mar 18 2021 at 19:37):

Where is your function of the form P -> Q which you're applying?

It's in h2

#### Kevin Buzzard (Mar 18 2021 at 19:49):

if h2 is of the form P -> Q then you should apply h2 instead, and it will work as long as your goal is Q. You are applying a theorem of the form "P or Q is true" and this isn't a function so you can't apply it.

#### Iocta (Mar 18 2021 at 19:52):

Er that's not right. h2 is P -> Q and I have P in goal. I think I should be able to say P is either true or it isn't. In case it's true, that's sufficient; in case it isn't I'm gonna try to find a contradiction.

#### Kevin Buzzard (Mar 18 2021 at 19:53):

Sure you can do that but apply doesn't do that. Maybe you want the by_cases tactic?

#### Kevin Buzzard (Mar 18 2021 at 19:54):

Oh if P is your goal then maybe by_contra is a quicker way to get where you want to go

#### Kevin Buzzard (Mar 18 2021 at 19:54):

Aah -- you use cases to split P or Q into a P line and a Q line so maybe another approach is to just change your apply to a cases. But by_contra will get you there more quickly.

#### Eric Wieser (Mar 18 2021 at 19:58):

That goal looks untrue to me

#### Kevin Buzzard (Mar 18 2021 at 20:00):

∃ (a b : ℝ), (a < b → s = (Ioc a b)) should surely be "a < b and s = ...". Otherwise such a and b always exist, just take a=1 and b=0.

#### Iocta (Mar 18 2021 at 20:03):

Like this? in_semialgebra := λ s, s = ∅ ∨ ∀ (a b : ℝ), (a < b ∧ s = (Ioc a b)),

#### Kevin Buzzard (Mar 18 2021 at 20:05):

That looks right, but why not just drop a < b and the s = emptyset as well, because when a>=b Ioc a b is just the empty set anyway.

#### Iocta (Mar 18 2021 at 20:08):

Oh that's much nicer

#### Kevin Buzzard (Mar 18 2021 at 20:09):

It's crazy how these things sometimes come out really super-nicely sometimes.

#### Iocta (Mar 18 2021 at 20:12):

I think I missed something. If the statement is just  in_semialgebra := λ s, ∀ (a b : ℝ), s = (Ioc a b), then semialgebra_empty will ask me to show that forall a b, Ioc a b = emptyset, which doesn't seem true.

#### Kevin Buzzard (Mar 18 2021 at 20:13):

There's something wrong with compl as well. Right now you can just let c = {s^compl}. If you restrict to all the elements of c being in your semialgebra then you can't make the complement of [0,1) because every set in your semialgebra has finite measure and so a finite union will do too. I think you might need the infinity versions of Ioc. I've forgotten what they're called though.

Iic?

#### Kevin Buzzard (Mar 18 2021 at 20:14):

yes it could well be that

docs#set.Iic

#### Kevin Buzzard (Mar 18 2021 at 20:15):

Yes, that. But I don't want to tell you what your semialgebra is -- it's your definition.

#### Iocta (Mar 18 2021 at 20:17):

I'm trying to copy image.png

#### Iocta (Mar 18 2021 at 20:18):

But one dimensional for now

#### Kevin Buzzard (Mar 18 2021 at 20:19):

note the possibility that a and b can be infinity.

#### Iocta (Mar 18 2021 at 20:19):

Well I guess I was sorta mixing that with image.png from https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras

#### Iocta (Mar 18 2021 at 20:19):

But maybe those definitions are actually not talking about the same object

(deleted)

#### Iocta (Mar 18 2021 at 20:26):

Yeah this can't be right

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example : semialgebra ereal := {
in_semialgebra := λ s, ∀ (a b : ereal), s = (Ioc a b),
semialgebra_empty := begin
intros a b,
-- a b: ereal
-- ⊢ ∅ = Ioc a b
end,
semialgebra_inter := begin
sorry,
end,
semialgebra_compl := begin
sorry
end
}

#### Iocta (Mar 18 2021 at 20:32):

Gotta be

example : semialgebra ereal := {
in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
semialgebra_empty := ⟨0, 0, sorry⟩,
semialgebra_inter := begin
sorry,
end,
semialgebra_compl := begin
sorry
end

#### Eric Wieser (Mar 18 2021 at 20:44):

Isn't that what I posted earlier?

#### Iocta (Mar 18 2021 at 20:49):

It's very close, also changed real to ereal

#### Iocta (Mar 19 2021 at 00:31):

I'm trying to make a finset with this these two elements but Lean doesn't know how to put the elements in the finset.

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

example : semialgebra ereal := {
in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
semialgebra_empty := ⟨0, 0, sorry⟩,
semialgebra_inter := begin
intros s1 s2 h1 h2,
cases h1 with a1 ha1,
{
cases ha1 with b1 hb1,
{
cases h2 with a2 ha2,
{
cases ha2 with b2 hb2,
use a1 ⊔ a2,
use b1 ⊓ b2,
rw [hb1, hb2, Ioc_inter_Ioc],
},
},
},
end,
semialgebra_compl := begin
intros s hs,
cases hs with a h,
cases h with b h,
rw h,
have t : finset (set ereal) := {(Iic a) , (Ioi b)},
-- failed to synthesize type class instance for
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ has_insert ?m_1 (finset (set ereal))
-- state:
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ ∃ (c : finset (set ereal)), ⋃₀↑c = (Ioc a b)ᶜ
end
}

#### Scott Morrison (Mar 19 2021 at 00:42):

Are you just missing decidable instances? What happens if you open_locale classical, or use classical at the beginning of the proof?

Yeah that was it

#### Iocta (Mar 19 2021 at 08:44):

How can I solve this?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical

lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ  = Iic a ∪ Ioi b :=
begin
sorry,
end

#### Iocta (Mar 19 2021 at 08:51):

I think it's true

#### Johan Commelin (Mar 19 2021 at 08:55):

Does ext get you started?

#### Eric Wieser (Mar 19 2021 at 11:01):

rw [mem_union_eq, mem_Ioi, mem_Iic, mem_compl_eq, mem_Ioc] will then get you most of the way to finished

#### Eric Wieser (Mar 19 2021 at 11:04):

I think it might be worth PRing that lemma, once golfed to:

lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ = Iic a ∪ Ioi b :=
set.ext $λ _, not_and_distrib.trans (or_congr not_lt not_le)  #### Eric Wieser (Mar 19 2021 at 11:04): Along with the other three variants of o and c #### Iocta (Mar 19 2021 at 21:52): This works now. How can I make it shorter? import measure_theory.measure_space import data.real.ereal open measure_theory measure_theory.measure_space classical set real open_locale classical structure semialgebra (α : Type*) := (in_semialgebra : set α → Prop) (semialgebra_empty : in_semialgebra ∅) (semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2)) (semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ) lemma compl_Ioc (a b : ereal) : (Ioc a b)ᶜ = Iic a ∪ Ioi b := set.ext$ λ _, not_and_distrib.trans (or_congr not_lt not_le)

example : semialgebra ereal := {
in_semialgebra := λ s, ∃ (a b : ereal), s = (Ioc a b),
semialgebra_empty := ⟨0, 0, by simp only [mem_empty_eq, forall_const, not_false_iff, Ioc_self],⟩,
semialgebra_inter := begin
intros s1 s2 h1 h2,
cases h1 with a1 ha1,
{
cases ha1 with b1 hb1,
{
cases h2 with a2 ha2,
{
cases ha2 with b2 hb2,
use a1 ⊔ a2,
use b1 ⊓ b2,
rw [hb1, hb2, Ioc_inter_Ioc],
},
},
},
end,
semialgebra_compl := begin
intros s hs,
cases hs with a h,
cases h with b h,
rw h,
let t : finset (set ereal) := {(Iic a) , (Ioi b)},
use t,
have: ⋃₀↑t =  (Iic a) ∪ (Ioi b),
from by simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
rw [this],
rw [compl_Ioc],
end
}

#### Eric Wieser (Mar 19 2021 at 21:59):

Yours intros and four cases tactics can be combined into a single rintros

#### Eric Wieser (Mar 19 2021 at 22:00):

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩

#### Eric Wieser (Mar 20 2021 at 10:14):

Here's how I'd golf the whole thing:

example : semialgebra ereal := {
in_semialgebra := λ s, ∃ (a b : ereal), s = Ioc a b,
semialgebra_empty := ⟨0, 0, (Ioc_self _).symm⟩,
semialgebra_inter := begin
rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
exact ⟨a1 ⊔ a2, b1 ⊓ b2, Ioc_inter_Ioc⟩,
end,
semialgebra_compl := begin
rintros s ⟨a, b, rfl⟩,
refine ⟨{Iic a, Ioi b}, eq.trans _ (compl_Ioc _ _).symm⟩,
simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
end }

#### Iocta (Mar 20 2021 at 20:43):

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩, works but if I replace it with rintros s1 s2 ⟨a1, b1, _⟩ ⟨a2, b2, _⟩, then it doesn't work. What is the difference?

#### Eric Wieser (Mar 20 2021 at 20:50):

rfl is like introducing h then immediately doing rw h

#### Eric Wieser (Mar 20 2021 at 20:50):

Although that's a bit of a simplification

#### Iocta (Mar 20 2021 at 20:51):

Whereas the _ is just introducing h?

#### Iocta (Mar 20 2021 at 21:00):

rintros s1 s2 ⟨a1, b1, h1⟩ ⟨a2, b2, h2⟩,
rw [h1, h2],

does work

#### Eric Wieser (Mar 20 2021 at 21:37):

Yeah, _ just tells lean to pick a name for you

#### Iocta (Mar 21 2021 at 04:46):

This works, what does a shorter version look like?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))

lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) : s1 = s2ᶜ :=
begin
ext,
split;
{
intro h,
simp only [mem_compl_eq] at *,
finish,
},
end

example : algebra' ℤ := {
in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
algebra_empty :=
⟨finset.empty, or.inl rfl⟩,
algebra_compl := begin
intros s hs,
cases hs with t ht,
cases ht with h ht,
{
use t,
rw [compl_compl],
right,
exact h,
},
{
use t,
left,
exact ht,
}
end,
algebra_union := begin
rintros s1 s2 ⟨t1, h1⟩ ⟨t2, h2⟩,
cases h1,
{
cases h2,
{
use t1 ∪ t2,
left,
simp only [finset.coe_union],
simp only [*],
},
{
use t2.filter (λx, x ∉ s1),
right,
rw [compl_union],
ext,
simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
split,
simp only [*, and_imp, finset.mem_coe] at *,
{
intros h h',
split,
{
have: s2 = t2ᶜ,
from by {
apply eq_compl_of_compl_eq,
exact h2,
},
simp only [*, not_not, finset.mem_coe, mem_compl_eq] at *,
},
{ exact h, },
},
{
intros h,
split,
{ exact h.2,  },
{
cases h,
rw [←mem_compl_eq],
simp only [*, finset.mem_coe] at *,
},
},
},
},
{
cases h2,
{
use t1.filter (λx, x ∉ s2),
right,
rw [compl_union],
ext,
split,
{
intro h,
simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
},
{
intro h,
have: s1 = t1ᶜ,
from by {
apply eq_compl_of_compl_eq,
exact h1,
},
{
simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
},
},
},
{
use t1.filter (λx, x ∈ t2),
have h1': s1 = t1ᶜ,
from by {
apply eq_compl_of_compl_eq,
exact h1,
},
have: s2 = t2ᶜ,
from by {
apply eq_compl_of_compl_eq,
exact h2,
},
right,
ext,
simp only [*, mem_sep_eq, compl_union, mem_inter_eq, iff_self, finset.mem_coe, finset.coe_filter] at *,
},
},
end
}

#### Kevin Buzzard (Mar 21 2021 at 08:04):

"have, from by apply exact" can all be done in one line, and one has to question whether it's even necessary given that you're about to close the goal with a simp * -- just throw the proof directly into the list of things in the list

#### Kevin Buzzard (Mar 21 2021 at 08:04):

intros, cases can be done with rintro

#### Kevin Buzzard (Mar 21 2021 at 08:05):

Did you try library_search for eq_compl_of_compl_eq?

#### Iocta (Mar 21 2021 at 08:16):

What is the rintros-only version of rintros s ⟨t, ht⟩, cases ht with h,?

#### Iocta (Mar 21 2021 at 08:17):

library_search didn't work for eq_compl_of_compl_eq ("excessive memory consumption")

#### Kevin Buzzard (Mar 21 2021 at 08:21):

Try looking for the iff version? The rintros version probably replaces ht with (h1 | h2)

#### Iocta (Mar 21 2021 at 08:25):

I tried replacing the have/from like simp only [*, not_not, finset.mem_coe, mem_compl_eq, eq_compl_of_compl_eq, h2] at *, but it said invalid simplification lemma 'eq_compl_of_compl_eq'

#### Kevin Buzzard (Mar 21 2021 at 08:27):

Indeed that is a useless simp lemma by itself. I'm suggesting you add the full proof ie eq_compl_of_compl_eq h1

#### Iocta (Mar 21 2021 at 08:28):

Replacing rintros s ⟨t, ht⟩, cases ht with h, with rintros s ⟨t, ⟨h1 | h2⟩⟩,  leaves me with image.png

#### Kevin Buzzard (Mar 21 2021 at 08:28):

You can just use simp to close goals, you don't need all this simp only stuff

#### Iocta (Mar 21 2021 at 08:29):

I read somewhere that it's bad style to just use simp because the simp rules change over time, so I normally write squeeze_simp and just use whatever it says

#### Kevin Buzzard (Mar 21 2021 at 08:29):

You need round brackets like I used, not pointy ones. Sorry I can't help more, I'm not at lean right now.

#### Kevin Buzzard (Mar 21 2021 at 08:30):

It's bad style to use simp to not close a goal. If it's solving the goal it's fine.

#### Iocta (Mar 21 2021 at 08:33):

can all be done in one line

what are the rules for what's done in a single line?

#### Iocta (Mar 21 2021 at 08:34):

btw dunno what's wrong with those ()in the screenshot but it always wraps weird like that when there's a \compl

#### Iocta (Mar 21 2021 at 08:36):

Try looking for the iff version?

lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) (x : ℤ) : x ∈ s1 ↔ x ∈ s2ᶜ :=
begin
library_search,
end

didn't work either

#### Eric Wieser (Mar 21 2021 at 09:13):

I think Kevin is describing

lemma eq_compl_iff_compl_eq (s1 s2: set ℤ) :
s1 = s2ᶜ ↔ s1ᶜ = s2 :=
begin
library_search,
end

does that work?

No

#### Eric Wieser (Mar 21 2021 at 18:52):

How about the statement function.involutive (has_compl.compl : set X \to set X)?

#### Iocta (Mar 21 2021 at 18:58):

If you mean

example (X : Type) : function.involutive (has_compl.compl : set X → set X) := begin
library_search,
end

then no

#### Kevin Buzzard (Mar 21 2021 at 19:08):

It's in there somewhere. Why not just read data.set.basic? Find the section on compl.

#### Iocta (Mar 21 2021 at 20:04):

Maybe it's in a form I don't recognize, but I don't see it. https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#lemmas-about-complement

#### Kevin Buzzard (Mar 21 2021 at 20:41):

There's also a bunch of stuff in order/boolean_algebra but I can't see it there either. Here are some shorter proofs:

import tactic
import data.set.basic

namespace set

variable {α : Type*}

lemma eq_compl_of_compl_eq {s1 s2: set α} : s1ᶜ = s2 → s1 = s2ᶜ :=
begin
rintro rfl,
exact (compl_compl s1).symm,
end

lemma eq_compl_iff_compl_eq (s1 s2 : set α) : s1ᶜ = s2 ↔ s1 = s2ᶜ :=
⟨eq_compl_of_compl_eq, λ h, (eq_compl_of_compl_eq h.symm).symm⟩

end set

#### Bryan Gin-ge Chen (Mar 21 2021 at 20:48):

These should definitely be added to mathlib (in order/boolean_algebra).

#### Iocta (Mar 21 2021 at 21:11):

Why is the have necessary?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))

lemma eq_compl_of_compl_eq (s1 s2: set ℤ) (h : s1ᶜ = s2) : s1 = s2ᶜ :=
begin
ext,
split;
{
intro h,
simp only [mem_compl_eq] at *,
finish,
},
end

example : algebra' ℤ := {
in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
algebra_empty :=
⟨finset.empty, or.inl rfl⟩,
algebra_compl := begin
rintros s ⟨t, ht⟩, cases ht with h,
{ use t, rw [compl_compl], right, exact h, },
{ use t, left, exact ht, }
end,
algebra_union := begin
rintros s1 s2 ⟨t1, (h11 |h12)⟩ ⟨t2, (h21 | h22)⟩,
{
use t1 ∪ t2,
left,
simp only [finset.coe_union, *],
},
{
use t2.filter (λx, x ∉ s1),
right,
rw [compl_union],
ext,
simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
split,
simp only [*, and_imp, finset.mem_coe] at *,
{
intros h h',
split,
{ -- have: s2 = t2ᶜ, from by {  apply eq_compl_of_compl_eq, exact h22, },
simp [*, eq_compl_of_compl_eq s2, eq_compl_of_compl_eq t2ᶜ] at *,  },
{ exact h, },
},
{
intros h,
split,
{ exact h.2,  },
{ cases h,
rw [←mem_compl_eq],
simp only [*, finset.mem_coe] at *,   },
},
},
{
use t1.filter (λx, x ∉ s2),
right,
rw [compl_union],
ext,
split,
{ intro h, simp [*] at *, },
{ intro h, { simp [*, eq_compl_of_compl_eq s1] at *,}, },
},
{
use t1.filter (λx, x ∈ t2),
right,
ext,
simp [*, eq_compl_of_compl_eq s1, eq_compl_of_compl_eq s2] at *,
},
end
}

simp_all tactic failed to simplify
state:
s1 s2 : set ℤ,
t1 : finset ℤ,
h11 : s1 = ↑t1,
t2 : finset ℤ,
h22 : s2ᶜ = ↑t2,
x : ℤ,
h : x ∉ t1,
h' : x ∉ s2
⊢ x ∈ t2

#### Iocta (Mar 21 2021 at 21:13):

Anyway that's a good reduction in verbosity, but still pretty large

#### Damiano Testa (Mar 22 2021 at 14:16):

You may want to double-check, but I think that this is a simplified version of what you had:

lemma compl_eq_iff {α : Type*} (s1 s2 : set α) : s1ᶜ = s2 ↔ s2ᶜ = s1 :=
by refine ⟨_, _⟩; rintros rfl; exact compl_compl _

example : algebra' ℤ := {
in_algebra := λs, ∃ (t : finset ℤ), (s = t) ∨ (sᶜ = t),
algebra_empty :=
⟨finset.empty, or.inl rfl⟩,
algebra_compl := begin
rintro s ⟨t, rfl | h⟩,
{ exact ⟨t, or.inr (compl_compl ↑t)⟩ },
{ exact ⟨t, or.inl h⟩ }
end,
algebra_union := begin
rintro s1 s2 ⟨t1, rfl | h⟩ ⟨t2, rfl | k⟩,
{ exact ⟨t1 ∪ t2, or.inl (finset.coe_union _ _).symm⟩ },
{ rw ← (compl_eq_iff _ _).mp k,
exact ⟨t2.filter (λx, x ∉ t1), or.inr (ext (λ x, by simp [and_comm]))⟩ },
{ rw ← (compl_eq_iff _ _).mp h,
exact ⟨t1.filter (λ x, x ∉ t2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
{ rw ← (compl_eq_iff _ _).mp h,
exact ⟨t1.filter (λx, x ∉ s2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
end }

#### Damiano Testa (Mar 22 2021 at 14:35):

Also, while I have not worked with it, it might be better to make implicit some of the inputs in your definition of algebra':

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ {s : set α}, in_algebra s → in_algebra sᶜ)  -- made s implicit
(algebra_union : ∀ {s1 s2 : set α}, in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))  -- made s1 s2 implicit

#### Iocta (Mar 22 2021 at 19:58):

That's quite an improvement! Thanks @Damiano Testa

#### Iocta (Mar 24 2021 at 19:14):

How can I express "the set of finite disjoint unions of sets in S"?
image.png

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))

structure semialgebra (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), sUnion (c : set (set α)) = sᶜ)

#### Kevin Buzzard (Mar 24 2021 at 19:19):

You could define it recursively. Or you might want to check that the finite disjoint unions are just the same as the finite unions, which would be easier to define and work with -- I think they are.

#### Iocta (Mar 24 2021 at 19:26):

by 'check that ...' do you mean check that this result holds for finite unions in general?

(deleted)

#### Kevin Buzzard (Mar 24 2021 at 19:50):

I can't make sense of your lemma 1.1.3. How does one see that "the definition of S implies S_i^c \in S-bar"? I can't immediately see how to deduce it from your formal definition of semialgebra -- you know that the complement is a union of things in the semialgebra but you don't know the union is disjoint, right?

#### Kevin Buzzard (Mar 24 2021 at 19:51):

For me, the algebra generated by the semialgebra seems to naturally be the finite union of elements of the semialgebra and then the proof that it's an algebra goes through; moreover it's clearly the smallest algebra containing the semialgebra, at least if we go via the definitions you have formalised.

#### Iocta (Mar 24 2021 at 20:51):

This text does use 'disjoint' in the definition of semialgebra image.png
so maybe I should try to include that in my lean semialgebra definition

#### Iocta (Mar 24 2021 at 20:51):

Or maybe that's unnecessary complication

#### Iocta (Mar 24 2021 at 21:06):

Is that like this?

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α → Prop)
(semialgebra_empty : in_semialgebra ∅)
(semialgebra_inter : ∀ (s1 s2 : set α), in_semialgebra s1 → in_semialgebra s2 → in_semialgebra (s1 ∩ s2))
(semialgebra_compl : ∀ (s : set α), in_semialgebra s → ∃ c : finset (set α), (∀ (x  ∈ c) (y ∈ c),  x ∩ y = ∅) ∧ sUnion (c : set (set α)) = sᶜ)

#### Kevin Buzzard (Mar 25 2021 at 08:12):

If you change the definition from the book then you'll have a different definition. Your definition of pairwise disjoint above is incorrect because you can have x=y. There might already be a way of saying "pairwise disjoint" in mathlib but I don't personally know it

#### Eric Wieser (Mar 25 2021 at 08:33):

docs#complete_lattice.independent I think is equivalent for sets?

Last updated: May 13 2021 at 00:41 UTC


text:
# The Unpolarized Shafarevich Conjecture for K3 Surfaces

-
Yiwei She , Columbia University
Fine Hall 214

Shafarevich made the following conjecture for higher genus curves: the set of isomorphism classes of genus g curves over K (a number field) with good reduction outside S (a fixed finite set of primes) is finite.  Faltings proved this and the analogous conjecture for abelian varieties of given degree. Zarhin proved this finiteness across all degrees. Using Faltings’ theorem, Andre proved the finiteness of K3 surfaces (over K, S) of a given degree. We prove the analog of Zarhin’s theorem, i.e. there are still finitely many K3 surfaces across all degrees.


text:
# Lesson 25

Using Linear Relations to Solve Problems

## 25.1: Buying Fruit (5 minutes)

### Warm-up

Students write expressions and equations representing total cost. The purpose of this activity is to support students in writing the equation for the “Ordering Fish” activity.

### Launch

Arrange students in groups of 2. Display questions for all to see. Give 2 minutes quiet think time, followed by 2 minutes partner discussion then whole-class discussion.

### Student Facing

For each relationship described, write an equation to represent the relationship.

1. Grapes cost $2.39 per pound. Bananas cost$0.59 per pound. You have $15 to spend on $$g$$ pounds of grapes and $$b$$ pounds of bananas. 2. A savings account has$50 in it at the start of the year and $20 is deposited each week. After $$x$$ weeks, there are $$y$$ dollars in the account. ### Student Response Teachers with a valid work email address can click here to register or sign in for free access to Student Response. ### Anticipated Misconceptions Some students may not be sure how to approach writing the scenario as an equation. For these students, suggest that they make a table of possible prices based on the amount of fruit purchased. ### Activity Synthesis The purpose of this discussion is to have students explain strategies for writing equations for real-world scenarios. Ask students to share what they discussed with their partners by asking: • “What did each of the variables mean in the situations?” (Since we want a price based on the number of pounds of fruit, $$b$$ and $$g$$ represent the amount of bananas and grapes purchased. For the savings account, the $$x$$ was the number of weeks, and the $$y$$ was number of dollars.) • “Was the slope for each of these equations positive or negative? Why does that make sense with the scenario?” (For the fruit, the slope was negative, which makes sense because if you buy more of one fruit, you have to buy less of the other. For the savings account, the slope is positive, which makes sense because the more weeks go by, the more money will be in the account.) ## 25.2: Five Savings Accounts (25 minutes) ### Activity Given a graph with five lines representing changes in bank account balance over time, students write equations and interpret how points represent solutions. The activity also connects to and contextualizes students’ prior understanding of slope and intercepts, and lays the foundation for the coming unit on systems of equations by considering what points of intersection of lines and non-intersecting lines represent. ### Launch Display the image from the lesson for all to see and ask the students to consider line $$a$$. Invite 2–3 students to describe in words what line $$a$$ shows. If no students bring it up, tell students that they saw this line before in the warm-up, and they wrote an equation for it. Instruct students that for #1, they should not choose line $$a$$. Arrange students in groups of 3–4. Groups work for about 10 minutes, followed by a whole-class discussion. Representation: Internalize Comprehension. Activate or supply background knowledge. Allow students to use calculators to ensure inclusive participation in the activity. Supports accessibility for: Memory; Conceptual processing Conversing: MLR8 Discussion Supports. Use this routine to support discussion about the question, “What can we say about the points where two lines cross?” Invite students work with a partner to select a few of the intersection points to discuss (between lines $$a$$ and $$c$$, $$a$$ and $$e$$, $$h$$ and $$c$$, $$h$$ and $$d$$, $$h$$ and $$e$$, and $$d$$ and $$e$$). Consider providing these sentence frames for pairs to use: “Lines _ and _ cross at the point _ and this tells me that . . . . I know this because . . . .” Encourage students to make explicit references to the number of weeks and dollar amounts that are represented. This will help students communicate about the point where two lines intersect in the context of a real-world situation. Design Principle(s): Support sense-making; Cultivate conversation ### Student Facing Each line represents one person’s weekly savings account balance from the start of the year. 1. Choose one line and write a description of what happens to that person's account over the first 17 weeks of the year. Do not tell your group which line you chose. 2. Share your story with your group and see if anyone can guess your line. 3. Write an equation for each line on the graph. What do the slope, $$m$$, and vertical intercept, $$b$$, in each equation mean in the situation? 4. For which equation is $$(1,70)$$ a solution? Interpret this solution in terms of your story. 5. Predict the balance in each account after 20 weeks. ### Student Response Teachers with a valid work email address can click here to register or sign in for free access to Student Response. ### Activity Synthesis Students should understand that points on a line show solutions to the equation of the line. Discuss with students: • “What can we say about the points where two lines cross?” (The accounts had the same amount of money at the same time.) • “How do the slopes of the lines help to tell the story from the graph?” (The slope tells us whether a person is spending or saving each week.) • “What does your answer to question 3 tell us about their rates of saving?” (By knowing the value of the slope, we can compare who is spending or saving more quickly or more slowly.) ## 25.3: Fabulous Fish (20 minutes) ### Activity Students represent a scenario with an equation and use the equation to find solutions. They create a graph (either with a table of values or by using two intercepts), interpret points on the graph, and interpret points not on the graph (MP2). ### Launch Allow about 10 minutes quiet think time for questions 1 through 4, then have students work with a partner to discuss questions 4 and 5. Look for students who define the variables or label the axes differently. This can be an opportunity to discuss the importance of defining what quantities your variables represent and that different graphs can represent the same information. Speaking, Listening: MLR2 Collect and Display. Listen for and record the language students use to discuss the statement “List two ways that you can tell if a pair of numbers is a solution to an equation.” Organize and group similar strategies in the display for students to refer back to throughout the lesson. For example, group strategies that reference the equation in one area and strategies that reference the graph in another area. This will help students solidify their understanding about solutions to an equation. Design Principle(s): Support sense-making; Maximize meta-awareness ### Student Facing The Fabulous Fish Market orders tilapia, which costs$3 per pound, and salmon, which costs $5 per pound. The market budgets$210 to spend on this order each day.

1. What are five different combinations of salmon and tilapia that the market can order?
2. Define variables and write an equation representing the relationship between the amount of each fish bought and how much the market spends.
3. Sketch a graph of the relationship. Label your axes.

4. On your graph, plot and label the combinations A—F.

A B C D E F
pounds of tilapia 5 19 27 25 65 55
pounds of salmon 36 30.6 25 27 6 4
5. Which of these combinations can the market order? Explain or show your reasoning.

6. List two ways you can tell if a pair of numbers is a solution to an equation.

### Anticipated Misconceptions

If students let $$x$$ be pounds of salmon, then the equation would be $$5x + 3y = 210$$ and the coordinates would be reversed. The intercepts of the graph would be $$(0,70)$$ and $$(42,0)$$. This is a good place to mention the importance of defining what quantities your variables represent.

### Activity Synthesis

Ask students to share some strategies for graphing and features of their graphs. Invite 2–3 students to display their graphs. Consider asking:

• "Was the slope of the line positive or negative? Why does that makes sense in this situation?" (In this relationship, as one quantity increases the other must decrease in order to keep the sum $$3x + 5y$$ constant.)
• "What was your strategy for graphing the relationship?" (Plotting points from question 1, using the table, figuring out the intercepts and connecting the line)
• "Why does it make sense for the graph to be only in quadrant I?" (You cannot purchase a negative amount of fish, so the $$x$$ and $$y$$ values cannot be negative.)
• "How is this situation different from the apples and oranges problem in a previous lesson?" (Buying $$\frac12$$ pound of fish is reasonable while buying $$\frac12$$ of an apple probably is not. )

Briefly reiterate key concepts: If a point is not on the graph of the equation then it is not a solution. The ordered pairs that are solutions to the equation all make the equation true and are all found on the line that is the graph of the equation.

A discussion could also include the detail that orders that are less than \$210 can also be considered to work, because there is money left over. That gives an opportunity to discuss the shape of the graph of $$3x + 5y \le 210$$.

## Lesson Synthesis

### Lesson Synthesis

Ask students to consider the real-world situations described in this lesson. Discuss:

• “Give an example of a solution to an equation that doesn’t make sense in the context it represents.” (Some values might not make sense in the context, like negative values. A length cannot be negative, for example.)
• “If some values make sense in the equation but not in the context, how could this impact the graph?” (We might only draw part of the line or draw some of the points that lie on the line.)


text:
location:  Publications → journals → CMB
Abstract view

# Asymptotic Existence of Resolvable Graph Designs

Published:2007-12-01
Printed: Dec 2007
• Peter Dukes
• Alan C. H. Ling
 Format: HTML LaTeX MathJax PDF PostScript

## Abstract

Let $v \ge k \ge 1$ and $\lam \ge 0$ be integers. A \emph{block design} $\BD(v,k,\lambda)$ is a collection $\cA$ of $k$-subsets of a $v$-set $X$ in which every unordered pair of elements from $X$ is contained in exactly $\lambda$ elements of $\cA$. More generally, for a fixed simple graph $G$, a \emph{graph design} $\GD(v,G,\lambda)$ is a collection $\cA$ of graphs isomorphic to $G$ with vertices in $X$ such that every unordered pair of elements from $X$ is an edge of exactly $\lambda$ elements of $\cA$. A famous result of Wilson says that for a fixed $G$ and $\lambda$, there exists a $\GD(v,G,\lambda)$ for all sufficiently large $v$ satisfying certain necessary conditions. A block (graph) design as above is \emph{resolvable} if $\cA$ can be partitioned into partitions of (graphs whose vertex sets partition) $X$. Lu has shown asymptotic existence in $v$ of resolvable $\BD(v,k,\lambda)$, yet for over twenty years the analogous problem for resolvable $\GD(v,G,\lambda)$ has remained open. In this paper, we settle asymptotic existence of resolvable graph designs.
 Keywords: graph decomposition, resolvable designs
 MSC Classifications: 05B05 - Block designs [See also 51E05, 62K10] 05C70 - Factorization, matching, partitioning, covering and packing 05B10 - Difference sets (number-theoretic, group-theoretic, etc.) [See also 11B13]

 top of page | contact us | privacy | site map |


text:
# IMDIV Function explained with examples step by step

Excel : IMDIV Function is extraordinary.Publishing high-quality reports/dashboard should be the aim of every data analyst, but this on its own isn’t enough for maximum success. For your reports to gain real traction, it needs to be fast, current and scalable. There are functions/methods like IMDIV Function in Excel which helps creating such reports, and this post gives advice on how to do it effectively.

In the tutorial, we will answer the question “How to use IMDIV Function in Excel?” with multiple examples using Excel. This will help in understanding where and why IMDIV Function should be use. Each artile I write will become a small step in automate creating and maintaining your projects. Similar examples will be shared to help you in your job or project. If you feel you realy need to know read ahead or else just scroll down to bottom to see code to use as it is.

IMDIV Function in Excel returns the quotient on division of two complex numbers.The IMDIV function syntax has the following arguments:

Excel : IMDIV Function

## How to add IMDIV Function in Excel?

The solution could have multiple approchesMain topics divided into 2 solutions approches which will be used to further drill down the solution Copy should use short, tight paragraphs and a variety of sub-headlines, lists, and indentations. Keep reading simple and easy

## IMDIV Function step by step guided approach

Quick quote bite!!!

A man may fulfill the object of his existence by asking a question he cannot answer… and attempting a task he cannot achieve. Oliver Wendell Holmes

Represented by Analytic Monk–

### Code solution

Code to be

=IMDIV(“-238+240i”,”10+24i”) Quotient of the two complex numbers in the formula. 5+12i The IMDIV function returns the division of the complex number (inumber) having both real & imaginary part. Syntax: =IMDIV (inumber1 , inumber2). inumber 1 :
The Excel Imdiv function calculates the quotient of two complex numbers (i.e. divides one complex number by another). The syntax of the function is: IMDIV(
IMDIV Function in Excel returns the quotient on division of two complex numbers. (i.e. divides one complex number from another). Syntax of IMDIV Function
IMDIV Function Syntax. =IMDIV (inumber1 , inumber2). Syntax Explanation: Sponsored Links. inumber 1 : First complex number
Use the IMDIV function. This function takes the numerator as its first argument, and the denominator as its second. Therefore, to find the current, enter =IMDIV
The IMDIV function returns the quotient of two complex numbers in x + yi or x + yj text format. IMDIV(z1,z2) = \frac{(a+bi)}{(
14-Sept-2020 · Welcome back to our regular A to Z of Excel Functions blog. Today we look at the IMDIV function.
An imaginary number is a complex number that
08-May-2020 · IMDIVFunction in Excel returns the quotient on division of two complex numbers. (i.e. divides one complex number from another). Syntax:
06-Apr-2021 · Documentation/Calc Functions/IMDIV
Syntax: IMDIV(Numerator; Denominator)
Equivalent Excel functions: IMDIV.

raw CODE content

monkidea.com/how-to-use-the-imdiv-function-in-excel-office-365/
=IMDIV (inumber1 , inumber2)

=IMDIV (A2, B2)

5 + i - ( 4 - i ) = (5 - 4) + ( i + i )= 1 + 2i

=IMDIV (A2, B2)

5 + i - ( 4 - i ) = (5 - 4) + ( i + i )= 1 + 2i
monkidea.com/advanced_excel_functions/advanced_excel_engineering_imdiv_function.htm
IMDIV (inumber1, inumber2)
monkidea.com/users/gnumeric/stable/CATEGORY_Complex.html.en
COMPLEX(x,y,i)

IMABS(z)

IMAGINARY(z)

IMARCCOS(z)

IMARCCOSH(z)

IMARCCOT(z)

IMARCCOTH(z)

IMARCCSC(z)

IMARCCSCH(z)

IMARCSEC(z)

IMARCSECH(z)

IMARCSIN(z)

IMARCSINH(z)

IMARCTAN(z)

IMARCTANH(z)

IMARGUMENT(z)

IMCONJUGATE(z)

IMCOS(z)

IMCOSH(z)

IMCOT(z)

IMCOTH(z)

IMCSC(z)

IMCSCH(z)

IMDIV(z1,z2)

IMEXP(z)

IMFACT(z)

IMGAMMA(z)

IMIGAMMA(a,z,lower,regularize)

IMINV(z)

IMLN(z)

IMLOG10(z)

IMLOG2(z)

IMNEG(z)

IMPOWER(z1,z2)

IMPRODUCT(z1,z2,…)

IMREAL(z)

IMSEC(z)

IMSECH(z)

IMSIN(z)

IMSINH(z)

IMSQRT(z)

IMSUB(z1,z2)

IMSUM(z1,z2,…)

IMTAN(z)

IMTANH(z)
monkidea.com/excel-functions/excel-imsum-function
=IMSUM("1+2i",3) // returns "4+2i"=IMSUM("3+4i","1+2i") // returns "4+6i"

=IMSUM("1+2i",3) // returns "4+2i"=IMSUM("3+4i","1+2i") // returns "4+6i"

=IMSUM(B6,C6)

=IMSUM(B6,C6)
monkidea.com/Advanced-excel-functions-advanced-excel-engineering-imdiv-function
IMDIV (inumber1, inumber2)

monkidea.com/how-to-use-the-imdiv-function-in-excel-office-365/
=IMDIV (inumber1 , inumber2)

=IMDIV (A2, B2)

5 + i - ( 4 - i ) = (5 - 4) + ( i + i )= 1 + 2i

=IMDIV (A2, B2)

5 + i - ( 4 - i ) = (5 - 4) + ( i + i )= 1 + 2i
monkidea.com/advanced_excel_functions/advanced_excel_engineering_imdiv_function.htm
IMDIV (inumber1, inumber2)

### Output achived after implementing the code

Show the final outcome of the code or the post.
Plus the text if we want to add
: End with a question or an idea that prompts the reader to like or share for future read…


text:
Tag Info

226

Let me offer one reason and one misconception as an answer to your question. The main reason that it is easier to write (seemingly) correct mathematical proofs is that they are written at a very high level. Suppose that you could write a program like this: function MaximumWindow(A, n, w): using a sliding window, calculate (in O(n)) the sums of all ...

77

(I am probably risking a few downvotes here, as I have no time/interest to make this a proper answer, but I find the text quoted (and the rest of the article cited) below to be quite insightful, also considering they are written by a well-known mathematician. Perhaps I can improve the answer later.) The idea, which I suppose isn't particularly distinct from ...

70

A common error I think is to use greedy algorithms, which is not always the correct approach, but might work in most test cases. Example: Coin denominations, $d_1,\dots,d_k$ and a number $n$, express $n$ as a sum of $d_i$:s with as few coins as possible. A naive approach is to use the largest possible coin first, and greedily produce such a sum. For ...

62

I immediately recalled an example from R. Backhouse (this might have been in one of his books). Apparently, he had assigned a programming assignment where the students had to write a Pascal program to test equality of two strings. One of the programs turned in by a student was the following: issame := (string1.length = string2.length); if issame then for ...

55

Allow me to start by quoting E. W. Dijkstra: "Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians." (from EWD498) Although what Dijkstra meant with `programming' differs quite a bit from the current usage, there is still some merit in this quote. The other answers have ...

50

Here is an algorithm for the identity function: Input: $n$ Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$ Otherwise, output $n$ Most people suspect this algorithm computes the identity function, but we don't know, and we can't prove it in the commonly accepted framework for mathematics, ZFC.

46

Lamport provides some ground for disagreement on prevalence of errors in proofs in How to write a proof (pages 8-9): Some twenty years ago, I decided to write a proof of the Schroeder-Bernstein theorem for an introductory mathematics class. The simplest proof I could find was in Kelley’s classic general topology text. Since Kelley was writing for a ...

39

One big difference is that programs typically are written to operate on inputs, whereas mathematical proofs generally start from a set of axioms and prior-known theorems. Sometimes you have to cover multiple corner cases to get a sufficiently general proof, but the cases and their resolution is explicitly enumerated and the scope of the result is implicitly ...

30

The best example I ever came across is primality testing: input: natural number p, p != 2 output: is p a prime or not? algorithm: compute 2**(p-1) mod p. If result = 1 then p is prime else p is not. This works for (almost) every number, except for a very few counter examples, and one actually needs a machine to find a counterexample in a realistic period ...

25

They say the problem with computers is that they do exactly what you tell them. I think this might be one of the many reasons. Notice that, with a computer program, the writer (you) is smart but the reader (CPU) is dumb. But with a mathematical proof, the writer (you) is smart and the reader (reviewer) is also smart. This means you can never afford to get ...

23

There are indeed programs like this. To prove this, let's suppose to the contrary that for every machine that doesn't halt, there is a proof it doesn't halt. These proofs are strings of finite length, so we can enumerate all proofs of length less than $s$ for some integer $s$. We can then use this to solve the halting problem as follows: Given a Turing ...

23

Ultimately, you'll need a mathematical proof of correctness. I'll get to some proof techniques for that below, but first, before diving into that, let me save you some time: before you look for a proof, try random testing. Random testing As a first step, I recommend you use random testing to test your algorithm. It's amazing how effective this is: in my ...

23

One issue that I think was not addressed in Yuval's answer, is that it seems you are comparing different animals. Saying "the code is correct" is a semantic statement, you mean to say that the object described by your code satisfies certain properties, e.g. for every input $n$ it computes $n!$. This is indeed a hard task, and to answer it, one has to look ...

22

First, let us make two maybe obvious, but important assumptions: _.random_item can choose the last position. _.random_item chooses every position with probability $\frac{1}{n+1}$. In order to prove correctness of your algorithm, you need an inductive argument similar to the one used here: For the singleton list there is only one possibility, so it is ...

21

Here's one that was thrown at me by google reps at a convention I went to. It was coded in C, but it works in other languages that use references. Sorry for having to code on [cs.se], but it's the only to illustrate it. swap(int& X, int& Y){ X := X ^ Y Y := X ^ Y X := X ^ Y } This algorithm will work for any values given to x and y, ...

18

What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter? I believe that the primary reasons are idempotency (gives the same results for the same inputs) and immutability (doesn't change). What if a mathematical proof could give different ...

16

There is a whole class of algorithms that is inherently hard to test: pseudo-random number generators. You can not test a single output but have to investigate (many) series of outputs with means of statistics. Depending on what and how you test you may well miss non-random characteristics. One famous case where things went horribly wrong is RANDU. It ...

16

This is not a secure encryption scheme. It is similar to a Hill cipher, and vulnerable to similar attacks. For instance, it is vulnerable to known-plaintext attacks: an attacker who observes a ciphertext E and knows the corresponding message M can recover the secret key and thus decrypt all other messages that were encrypted with the same key. The ...

14

I will use the following simple sorting algorithm as an example: repeat: if there are adjacent items in the wrong order: pick one such pair and swap else break To prove the correctness I use two steps. First I show that the algorithm always terminates. Then I show that the solution where it terminates is the one I want. For the first point,...

13

We are indeed assuming $P(k)$ holds for all $k < n$. This is a generalization of the "From $P(n-1)$, we prove $P(n)$" style of proof you're familiar with. The proof you describe is known as the principle of strong mathematical induction and has the form Suppose that $P(n)$ is a predicate defined on $n\in \{1, 2, \dotsc\}$. If we can show that ... 12 I agree with what Yuval has written. But also have a much simpler answer: In practice softwares engineers typically don't even try to check for correctness of their programs, they simply don't, they typically don't even write down the conditions that define when the program is correct. There are various reasons for it. One is that most software engineers ... 11 You need the line C(i:j) = 0 just before the innermost loop; otherwise, the code is incorrect. Assuming that line is in place, here is the (strongest possible) invariant just before the assignment in the innermost loop: \begin{align*} C_{IJ} &= \sum_{k=1}^{n} A_{Ik}B_{kJ} & \text{for allI$and$J$such that$1\le I < i$and$1\le J\le n$} \\ \... 11 No, your algorithm doesn't work. Consider if the array A is A = [1 1 1 1 1 2 2 3 3 3 3 3 3]. Then the array B will be B = [5 5 5 5 5 2 2 6 6 6 6 6 6]. The sum of B will be 65, and the length of B will be 13, so after division, we'll get the number 5. This is equal to the first element of B, so your algorithm will output "Yes". Nonetheless, not all ... 11 There are a lot of good answers already but there are still more reasons math and programming aren't the same. 1 Mathematical proofs tend to be much simpler than computer programs. Consider the first steps of a hypothetical proof: Let a be an integer Let b be an integer Let c = a+b So far the proof is fine. Let's turn that into the first ... 10 There is no (one) formal definition of "optimal substructure" (or the Bellman optimality criterion) so you can not possibly hope to (formally) prove you have it. You should do the following: Set up your (candidate) dynamic programming recurrence. Prove it correct by induction. Formulate the (iterative, memoizing) algorithm following the recurrence. 10 Cryptosystems which are algebraic in nature are amenable to algebraic cryptanalysis. If you are trying to design a secure cryptosystem for actual use, there is one important maxim that you should keep in mind: Don't design your own cryptosystem! It is easy to design weak cryptosystems. Off-the-shelf cryptosystems have withstood breaking attempts by the ... 10 I like Yuval's answer, but I wanted to riff off of it for a bit. One reason you might find it easier to write Math proofs might boil down to how platonic Math ontology is. To see what I mean, consider the following: Functions in Math are pure (the entire result of calling a function is completely encapsulated in the return value, which is deterministic and ... 9 Proving that a program is "thread safe" is hard. It is possible, however, to concretely and formally define the term "data race." And it is possible to determine whether an execution trace of a specific run of a program does or does not have a data race in time proportional to the size of the trace. This type of analysis goes back at least to 1988: ... 9 2D local maximum input: 2-dimensional$n \times n$array$A$output: a local maximum -- a pair$(i,j)$such that$A[i,j]$has no neighboring cell in the array that contains a strictly larger value. (The neighboring cells are those among$A[i, j+1], A[i, j-1], A[i-1, j], A[i+1, j]$that are present in the array.) So, for example, if$A$is$\$\begin{...

9

First off to answer your main question: there is no flaw in the proof. The point where you are not following the reasoning of the proof is that: E belongs to a cycle in the graph and to the MST. Not every other edge of the cycle are in the MST. If you look at your drawing, then either one of the edges towards the rest of the MST is redundant. Because ...

Only top voted, non community-wiki answers of a minimum length are eligible


text:
# Matriser latex, emma er europas mest prisbelønnede madras

Math Solver – Appar på Google Play

Matricies can be entered in the table or pasted into the text field as a tab-delimited glob of text. Correct latex is generated for any entered fractions. TypematrixpmatrixbmatrixBmatrixvmatrixVmatrixRowsCols. It’s well known that some rows of the arrays created by default with LaTeX are, by default, too close to each other. Here is a classical example.

Watch later. Share. Copy link. Info. Shopping.

## prevulcanized latex — Svenska översättning - TechDico

Vote. 2 ⋮ Vote. 2. Answered: Walter Roberson Dear all, I would need your advices to write a pretty matrix with latex.

### Admira Fusion från VOCO – Världens första helt keramiskt

4 layers of felt, 1'' of super soft latex, 3/4'' of firm latex, and a plush alpaca topper over the innerspring matrix. Stark hårspray Vavoom Matrix (250 ml) l Köp billigt online i Stockholm, Malmö, Uppsala, Västerås, Örebro ✓recensioner ✓ bösta pris ✓ köp Hårspray ➔ på  elektronisk som skannat pdf, word, Latex eller i annat format. Filens namn bör utformas så http://www.maths.lth.se/matematiklth/personal/ufn/matris/matrix.pdf. Matrix-serien är full av oförglömliga actionscener, fantastiska effekter fiction-juggernaut som gjorde latex till det coolaste det någonsin varit.

Sparad från cisforcostumes.tumblr.com  This is followed by the innerspring matrix below. 4 layers of felt, 1'' of super soft latex, 3/4'' of firm latex, and a plush alpaca topper over the innerspring matrix.
Is britannica a good source

In this video, Vince shows how to quickly write out matrices in LaTeX, using the amsmath package and the \pmatrix (for a matrix with curly brackets), \matrix (for a matrix with no brackets), and \vmatrix (used to denote the determinant of a matrix) commands. How to write an m⨉n matrix in LaTeX? Ask Question Asked 8 years, 7 months ago.
Lars westling bygg

excel vba delay
indebetou deutsch
plantagen grill speisekarte
hedemora trafikskolan
neglekt syndrom
jobbklar malmö

### C is For Costumes - Monica Bellucci as Persephone in Matrix

matrix is passed as an argument between \begin and \end commands. And this argument indicates that the matrix will be bound by which bracket?

Nettoskuld ebitda
sveriges elanvändning

### Köp LEXI No 6 Sängpaket 140 Fast Latex/Memory, Komplett

lp: Create left parenthesis: rp: Create right parenthesis: s In mathematics, particularly linear algebra, a zero matrix or null matrix is a matrix all of whose entries are zero.

## Fototapet Matrix Effekt Hintergrund • Pixers® - Vi lever för

But what if one of the entries in the matrix was a 2+10 instead of just being a 2. This shows that the lower row vector isn't properly aligned with the matrix, it just has it's left end aligned. I want to create a matrix with my results and then to obtain the output in latex code. However, the first column are natural number, and the second one are not integers, so I can´t create a matrix with different inputs (Am I right?). How can I do? Latex norm of a vector or a value \lVert x \rVert $$\lVert \vec{x} \rVert$$ \lVert \cos x \rVert $$\lVert \cos x \rVert$$ Adjust Latex norm for frac Takes a Python or MATLAB matrix and outputs a LaTeX table, a LaTeX matrix, or a complete LaTeX document (and optionally calls latex for compilation).

Just array to make the matrix and. Matrix (and other tabular or array ) constructions use & to denote the column delineation, not \quad : enter image description here \documentclass{article}  Are you using in-line delimiters around the math? E.g., $\begin{pmatrix} 2 \\ 4 \\ -2 \end{pmatrix}$. If you put another matrix inside these  Example#. Matrices. You must always use the amsmath package if you are going to use the following commands.