Zulip Chat Archive

Stream: maths

Topic: Cauchy integral formula


view this post on Zulip 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

view this post on Zulip 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)) : μ = ν

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 31 2020 at 04:44):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 31 2020 at 15:53):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 01 2020 at 03:09):

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

view this post on Zulip 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.

view this post on Zulip 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 C1C^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).

view this post on Zulip Yury G. Kudryashov (Nov 01 2020 at 03:37):

We can easily get partitions of unity after #4458

view this post on Zulip Yury G. Kudryashov (Nov 01 2020 at 04:13):

What do you think about merging our efforts?

view this post on Zulip 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,
[a,b]dω[a,b]ω\int_{[a,b]}d\omega - \int_{\partial[a,b]}\omega is o(volume)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.

view this post on Zulip 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,
[a,b]dω[a,b]ω\int_{[a,b]}d\omega - \int_{\partial[a,b]}\omega is o(volume)o(volume),

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


Last updated: May 14 2021 at 18:28 UTC