alternative proof of gauss integral #1584
Conversation
IshiguroYoshihiro
changed the title
There was a problem hiding this comment.
Is this a good file name?
| @@ -4,6 +4,9 @@ | |||
|
|
|||
| ### Added | |||
|
|
|||
| - in `theories/showcase` | |||
| + add new file `gauss_integral_alternative.v` | |||
There was a problem hiding this comment.
The new lemmas and definitions should also be added in the changelog
| (* # calculating gauss integrals by limit *) | ||
| (* ref: https://www.phys.uconn.edu/~rozman/Courses/P2400_17S/ *) | ||
| (* downloads/gaussian-integral.pdf *) | ||
| (* u (x : R) (y : R) : R == a function dominates gauss_fun over `[0, +oo[ *) |
There was a problem hiding this comment.
This should not be duplicated and the proper module imported. The module name in the original file also does not seem appropriate, it is worth considering to rearrange the original proof such that this alternative proof is more readable, and the symbols are available when appropriate.
| (* NB: some Notations and lemmas in gauss_integral are duplicated because *) | ||
| (* those are in Module or defined by `Let` so cannot be used directly. *) |
There was a problem hiding this comment.
Remove this when applying the comment above.
| (* PRed #1579 *) | ||
| Section ge0_nondecreasing_set_seq_cvg_integral. | ||
| Context {R : realType}. | ||
| Variables (S : (set R)^nat) (f : R -> \bar R). | ||
| Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). | ||
| Hypothesis (mf : (forall i, measurable_fun (S i) f)). | ||
| Hypothesis (f0 : forall i x, S i x -> 0 <= f x). | ||
|
|
||
| Notation mu := lebesgue_measure. | ||
|
|
||
| Lemma ge0_nondecreasing_set_seq_nondecreasing_integral_seq : | ||
| nondecreasing_seq (fun i => \int[mu]_(x in S i) f x). | ||
| Proof. | ||
| Admitted. | ||
|
|
||
| Lemma ge0_nondecreasing_set_seq_cvg_integral : | ||
| \int[mu]_(x in (S i)) f x @[i --> \oo] --> | ||
| \int[mu]_(x in \bigcup_i S i) f x. | ||
| Proof. | ||
| Admitted. | ||
|
|
||
| End ge0_nondecreasing_set_seq_cvg_integral. |
There was a problem hiding this comment.
This section needs to be remove, pending PR #1579
|
|
||
| Lemma max_y_ge0 : (0 <= max_y)%R. Proof. by rewrite mulr_ge0. Qed. | ||
|
|
||
| Definition helper (x : R) := (2 * x * expR (- x ^+ 2))%R. |
There was a problem hiding this comment.
This and the next definitions and lemmas are non-descriptive. I recommend finding a better name.
| (* in gauss_integral but as a Let *) | ||
| Lemma integral0y_gauss_ge0 : (0%E <= \int[mu]_(x in `[0%R, +oo[) (gauss_fun x)%:E)%E. | ||
| Proof. by apply: integral_ge0 => //= x _; rewrite lee_fin gauss_fun_ge0. Qed. |
There was a problem hiding this comment.
Use the original lemma and remove this.
|
|
||
| (* for lemmas only for integral yet *) | ||
| Lemma EFinK {R : realType} (x : R) : x = fine (EFin x). | ||
| Proof. by []. Qed. |
|
|
||
| Lemma int_substE x : (0 < x)%R -> | ||
| \int[mu]_(y in `[0%R, +oo[) (expR (- x ^+ 2 * oneDsqr y))%:E | ||
| = (\int[mu]_(x1 in `[0%R, +oo[) (gauss_fun x / x * gauss_fun x1)%:E). |
There was a problem hiding this comment.
| = (\int[mu]_(x1 in `[0%R, +oo[) (gauss_fun x / x * gauss_fun x1)%:E). | |
| = \int[mu]_(x1 in `[0%R, +oo[) (gauss_fun x / x * gauss_fun x1)%:E. |
|
|
||
| Let dudx x0 y0 : R := (u^~ y0)^`() x0. | ||
|
|
||
| Lemma int0yu_fin_num x : \int[mu]_(x0 in `[0%R, +oo[) (u x x0)%:E \is a fin_num. |
There was a problem hiding this comment.
Should this be using int0yu?
Motivation for this change
I added an alternative proof of gauss integral and placed it in
theories/showcase.This is an experimental approach to evaluating improper integral.
I have already separate reusable lemmas and made PRs ( #1579 is under review now), so this file intended to showcases the difference of proof strategy.
In contrast to the existing proof, this version mainly relies on lemmas related to integration over unbounded intervals.
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers