Cauchy integral formula

Stream: maths

[Yury G. Kudryashov]

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]

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]

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]

@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]

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

[Yury G. Kudryashov]

@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]

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

[Floris van Doorn]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

We can easily get partitions of unity after #4458

[Yury G. Kudryashov]

What do you think about merging our efforts?

[Heather Macbeth]

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]

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).

[Yury G. Kudryashov]

#10000 is ready for review (modulo docs and dependencies). It depends on #10906 (circle integral) which depends on #10895 (monotonicity of f : int → α) and #10788 (non-integrable functions).

[Yury G. Kudryashov]

@Jireh Loreaux Do you want to help with docs? This is a good way to study the code you're going to use.

[Yury G. Kudryashov]

(I can try to add missing docs myself tomorrow)

[Jireh Loreaux]

Sure, but I'll need a few days. Today I need to finish grading, and tomorrow we're celebrating our family Christmas.

[Yury G. Kudryashov]

Today I need to finish grading

I wish I had an option to finish my grading today.

[Jireh Loreaux]

I don't have a choice; grades due tomorrow.

[Yury G. Kudryashov]

And I have to grade 1 problem in >1.5K submissions. Not possible in 1 day.

[Yury G. Kudryashov]

@Jireh Loreaux I've started branch#YK-cauchy-deriv with a misleading name. Actually, I'm going to prove several versions of the max principle in this branch. E.g., have a look at this lemma.

[Jireh Loreaux]

sorry, that didn't take me directly to a specific lemma, which did you have in mind?

[Yury G. Kudryashov]

exists_eq_const_of_differentiable_of_bounded in cauchy_integral.lean

[Yury G. Kudryashov]

I added some docs to #10000. It's ready for review.

[Patrick Massot]

@Yury G. Kudryashov I think this PR is waiting for the resolution of this discussion.

[Yury G. Kudryashov]

Yes. I'll try to fix it tomorrow.