## Stream: maths

### Topic: Cauchy integral formula

#### Yury G. Kudryashov (Oct 31 2020 at 04:31):

I've started working on Cauchy integral formula. In this file you can find the following theorem:

def box_subadditive_on [decidable_eq ι] [preorder α] [ordered_add_comm_monoid M]
(f : (ι → α) → (ι → α) → M) (s : set (ι → α)) :=
∀ ⦃lo : ι → α⦄ (hlo : lo ∈ s) ⦃hi : ι → α⦄ (hhi : hi ∈ s) ⦃i x⦄,
lo i ≤ x → x ≤ hi i → f lo hi ≤ f lo (update hi i x) + f (update lo i x) hi

variables {s : set (ι → ℝ)} [ord_connected s]

lemma eq_of_forall_eventually_le_mul {f g : (ι → ℝ) → (ι → ℝ) → ennreal}
(hf : box_subadditive_on f s) (hg : @box_subadditive_on ι ℝ (order_dual ennreal) _ _ _ g s)
(Hc : ∀ (b ∈ s) (c > 0), ∀ᶠ p in 𝓝[(set.Iic b).prod (set.Ici b)] (b, b),
f (prod.fst p) p.2 ≤ c * g p.1 p.2) {lo hi} (hlo : lo ∈ s) (hhi : hi ∈ s)
(hle : lo ≤ hi) (h_inf : g lo hi < ⊤) : f lo hi = 0 :=
sorry


#### Yury G. Kudryashov (Oct 31 2020 at 04:39):

The lemma is formulated for ennreal-valued functions because it is useful to prove the following fact about measures:

lemma measure.ext_of_eventually_le_mul {μ ν : measure (ι → ℝ)} (h : ∀ b (c > 0), 𝓝[(set.Iic b).prod (set.Ici b)] (b, b),
max (μ (Icc p.1 p.2) - ν (Icc p.1 p.2)) (ν (Icc p.1 p.2) - μ (Icc p.1 p.2)) ≤ c * ∏ i, ennreal.of_real (p.2 i - p.1 i)) : μ = ν


#### Yury G. Kudryashov (Oct 31 2020 at 04:41):

For Cauchy theorem the real-valued version of first lemma should be applied to the same g lo hi= ∏ i, (hi i - lo i) and f lo hi = norm (contour integral of Pdx+Qdy - double integral of (Q'_x-P'_y)dxdy

#### Yury G. Kudryashov (Oct 31 2020 at 04:43):

@Patrick Massot This proof works in any dimension but is technically easier to the one you've mentioned several days ago. Namely, I don't prove the mean value theorem with equality. A version with inequality works just fine.

#### Yury G. Kudryashov (Oct 31 2020 at 04:44):

@Heather Macbeth @Alex Kontorovich Are you interested in :up:?

#### Yury G. Kudryashov (Oct 31 2020 at 04:49):

@Floris van Doorn The ext lemma mentioned above should be useful in the proof of the fact that the image of lebesgue under a diffeomorphism is lebesgue with density det (jacobian).

#### Yury G. Kudryashov (Oct 31 2020 at 04:50):

Currently this branch doesn't build because I've tried to add two more classes to algebraic/ordered hierarchy and failed.

#### Floris van Doorn (Oct 31 2020 at 07:28):

The ext lemma is still quite some ways off, since we don't even have n-ary product measures for n > 2, right?
I also cannot read hypothesis h. Is there an eventually in there?

#### Patrick Massot (Oct 31 2020 at 10:19):

It looks promising! To the other people reading this thread: Yury's message is probably impossible to understand if you don't read https://link.springer.com/article/10.1007/BF03024304 first

#### Yury G. Kudryashov (Oct 31 2020 at 12:29):

Floris van Doorn said:

The ext lemma is still quite some ways off, since we don't even have n-ary product measures for n > 2, right?
I also cannot read hypothesis h. Is there an eventually in there?

Added missing eventually. We can define Lebesgue measure on R^n as Haar measure.

#### Yury G. Kudryashov (Oct 31 2020 at 15:53):

BTW, an ext lemma & formula for measure.map in dimension 1 seems useful to me.

#### Heather Macbeth (Oct 31 2020 at 19:24):

First, here's the branch on which @Alex Kontorovich and I have been trying Goursat's theorem. Optimistically, I might say we're halfway to sorry-free. branch#triangles

#### Heather Macbeth (Oct 31 2020 at 19:25):

Yury G. Kudryashov said:

For Cauchy theorem the real-valued version of first lemma should be applied to the same g lo hi= ∏ i, (hi i - lo i) and f lo hi = norm (contour integral of Pdx+Qdy - double integral of (Q'_x-P'_y)dxdy

@Yury G. Kudryashov, would you envisage doing this directly for Cauchy (as you seem to suggest here) or deriving Stokes first?

#### Heather Macbeth (Oct 31 2020 at 19:29):

And which generality of domain? In the Acker article it's rectangles only, would that be your plan or would it be for more general domains (using some version of the manifolds-with-corners theory perhaps)?

#### Patrick Massot (Oct 31 2020 at 20:47):

Every proof of Stokes that I know about goes through rectangles first. You then need partitions of unity to get the general case.

#### Yury G. Kudryashov (Nov 01 2020 at 03:03):

@Heather Macbeth I saw your branch a few days ago, and I was doing the "other" half.

#### Yury G. Kudryashov (Nov 01 2020 at 03:09):

Namely, now I have a proof of the following fact: if $f\colon\mathbb R^n\to\mathbb R^n\to E$ is an additive function of a box in $\mathbb R^n$ (e.g., $f (a, b) = ∫_{[a, b]} dω-∫_{∂[a, b]}ω$, where $[a, b]=\{x | a\le x\le b\}$) and it is $o(volume)$ near each point, then it is zero.

#### Yury G. Kudryashov (Nov 01 2020 at 03:11):

Based on what I saw, you were working on the other half that will imply that we have this is_o.

#### Yury G. Kudryashov (Nov 01 2020 at 03:15):

I was going to do the following:

1. Prove Green's formula for rectangles with no $C^1$ requirement.
2. Deduce Cauchy/Goursat's theorem for rectangles.
3. Deduce Cauchy formula for a point inside a circle using a trick: explicitly parametrize the annulus by a rectangle (exp composed with a fractional linear map).
4. Deduce the fact that any complex differentiable function is analytic.
5. Deduce max principle (does not depend on 4).

#### Yury G. Kudryashov (Nov 01 2020 at 03:37):

We can easily get partitions of unity after #4458

#### Yury G. Kudryashov (Nov 01 2020 at 04:13):

What do you think about merging our efforts?

#### Heather Macbeth (Nov 01 2020 at 06:16):

For sure, let's merge the efforts -- @Alex Kontorovich, what do you think?

I am still getting my head round this different proof. Your lemma additive + o(volume) -> integral zero, this replaces the juggling with the quadrisect function in our branch, is that right? Our (very incomplete) inductive argument about subdividing into smaller and smaller triangles is replaced by your iteration next subdividing into smaller and smaller boxes?

So as you say, the lemma that remains to be proved is that, for a descending-to-a-point sequence of boxes/triangles,
$\int_{[a,b]}d\omega - \int_{\partial[a,b]}\omega$ is $o(volume)$, and judging from page 7 of the Acker article, the proof of this in general (for Green/Stokes) should be the same as the special case we've been working on for Cauchy/Goursat:

• prove things cancel exactly for $\omega$ constant or linear (we mostly have this for Cauchy-Goursat, but should generalize it to work for Green/Stokes)
• show that the second-order error term shrinks (we didn't start this yet).

These things together will do (1) and (2), and then the fun part (3)-(5) begins.

#### Patrick Massot (Nov 01 2020 at 20:28):

Heather Macbeth said:

So as you say, the lemma that remains to be proved is that, for a descending-to-a-point sequence of boxes/triangles,
$\int_{[a,b]}d\omega - \int_{\partial[a,b]}\omega$ is $o(volume)$,

The key point is this is almost the definition of $d\omega$ (it's the definition is you remove the first integral sign).

Last updated: May 14 2021 at 18:28 UTC