feat: Liouville Theorem for harmonic functions#35640
feat: Liouville Theorem for harmonic functions#35640kebekus wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
PR summary 8a897592b7Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 13074 | 1 | backward.isDefEq |
Current commit a3b8f36c17
Reference commit 8a897592b7
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
| theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ {f : ℂ → ℝ} | ||
| (hf : HarmonicOnNhd f univ) : | ||
| ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F univ) ∧ ((fun z ↦ (F z).re) = f) := by | ||
| let g := ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I) |
There was a problem hiding this comment.
This isn't how I would approach this. Instead, I recommend defining a harmonicConjugate function, and then proving that the function f + I * harmonicConjugate f is holomorphic. You can then add the existential statement as a consequence for convenience if you prefer.
|
|
||
| open Complex Real Set | ||
|
|
||
| set_option backward.isDefEq.respectTransparency false |
There was a problem hiding this comment.
Also, can you merge master and check that this is still necessary?
| set_option backward.isDefEq.respectTransparency false | |
| set_option backward.isDefEq.respectTransparency false in |
| theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant | ||
| (f : ℂ → ℝ) | ||
| (h_harm : HarmonicOnNhd f univ) | ||
| (h_bound : Bornology.IsBounded (range f)) : | ||
| ∀ z w, f z = f w := by |
There was a problem hiding this comment.
Does this really only work for ℝ-valued functions? Can't you take values in a finite dimensional inner product space? I thought it was true in that generality.
| /-- | ||
| **Morera's theorem for the complex plane** A continuous function on `ℂ` whose integrals on | ||
| rectangles vanish, has primitives. | ||
| -/ | ||
| theorem IsConservativeOn.isExactOn_univ (h₁ : Continuous f) (h₂ : IsConservativeOn f univ) : | ||
| IsExactOn f univ := by | ||
| use (wedgeIntegral 0 · f) | ||
| intro z _ | ||
| have h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1)) := h₂.mono (subset_univ _) | ||
| exact h₃.hasDerivAt_wedgeIntegral (by fun_prop) (by aesop) | ||
|
|
||
| /-- | ||
| **Morera's theorem for the complex plane** A holomorphic function on `ℂ` has | ||
| primitives. | ||
| -/ | ||
| theorem _root_.Differentiable.isExactOn_univ (hf : Differentiable ℂ f) : IsExactOn f univ := by | ||
| apply IsConservativeOn.isExactOn_univ hf.continuous | ||
| ((isConservativeOn_and_continuousOn_iff_isDifferentiableOn isOpen_univ).2 hf.differentiableOn).1 |
There was a problem hiding this comment.
Can you please do it for any open set instead, and then conclude these afterwards?
| theorem exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * (2 * π * I) := by | ||
| simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add'] | ||
|
|
||
| @[grind .] lemma re_eq_re_if_cexp_eq_cexp {x y : ℂ} (h : cexp x = cexp y) : |
There was a problem hiding this comment.
| @[grind .] lemma re_eq_re_if_cexp_eq_cexp {x y : ℂ} (h : cexp x = cexp y) : | |
| @[grind .] lemma re_eq_re_of_cexp_eq_cexp {x y : ℂ} (h : cexp x = cexp y) : |
j-loreaux
added
the
awaiting-author
2 participants
Implement Liouville's theorem for harmonic functions on the complex plane.
This material is used in Project VD, formalizing Value Distribution Theory for meromorphic functions on the complex plane.