Formalizing conformal maps

Stream: maths

[Yourong Zang]

Hello, I have written some codes for conformal maps between inner product spaces, which was previously discussed here. My code is available here, which is still a rough draft. The proofs and style were modified once, according to some very valuable comments from @Patrick Massot provided by Prof. Buzzard. I am extremely grateful for any suggestion. Some of the relatively trivial lemmas might be redundant but I was unable to find the appropriate alternatives in mathlib. Here is a file with shorter proofs but less compact statements.

Also, do we need partial derivatives to formalize Liouville's theorem on C^4 conformal mappings between Euclidean spaces?

Thanks in advance.

[Oliver Nash]

I have only glanced at this but it looks really great! If you are wondering what to do next, I suggest you carve off a small piece and turn it into a PR.

[Kevin Buzzard]

I played with some of the first 150 lines. Your code is really good! In the comments below I show you some more tips.

import tactic
import data.matrix.notation
import analysis.complex.basic
import geometry.manifold.charted_space
import analysis.normed_space.inner_product
import linear_algebra.matrix.to_linear_equiv
import geometry.euclidean.basic
import analysis.complex.isometry
import analysis.normed_space.finite_dimension

noncomputable theory

-- I personally like to have section names which are "obviously not namespaces"
-- so that when I see `end conformal_API` I will know it's not the end of a namespace

section conformal_API

def is_conformal_map {X Y : Type*}
[inner_product_space ℝ X] [inner_product_space ℝ Y] (f' : X →L[ℝ] Y) :=
∃ (c : ℝ) (hc : c ≠ 0) (lie : X ≃ₗᵢ[ℝ] Y), ⇑f' = (λ y, c • y) ∘ lie

def conformal_at
{X Y : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y]
(f : X → Y) (x : X) :=
∃ (f' : X →L[ℝ] Y), has_fderiv_at f f' x ∧ is_conformal_map f'

-- let's make an API for `conformal_at` before we start on `conformal`.
-- Let's do it in a namespace and set up variables for that namespace.

namespace conformal_at

variables {X Y Z : Type*}
  [inner_product_space ℝ X] [inner_product_space ℝ Y] [inner_product_space ℝ Z]

-- save some time by opening these
open linear_isometry_equiv continuous_linear_map

theorem differentiable_at {f : X → Y} {x : X} (h : conformal_at f x) :
differentiable_at ℝ f x := let ⟨_, h₁, _, _, _, _⟩ := h in h₁.differentiable_at

-- I can use `refl` now instead of `linear_isometry_equiv.refl`
theorem id (x : X) : conformal_at id x :=
⟨id ℝ X, has_fderiv_at_id _, 1, one_ne_zero, refl ℝ X, by ext; simp⟩

theorem const_smul {c : ℝ} (h : c ≠ 0) (x : X) : conformal_at (λ (x': X), c • x') x :=
-- no `by apply` needed
⟨c • continuous_linear_map.id ℝ X, has_fderiv_at.const_smul (has_fderiv_at_id x) c, c, h, refl ℝ X, by ext; simp⟩

-- putting conformal_at f x before the colon means you can `rintro` everything
theorem comp {f : X → Y} {g : Y → Z} {x : X} :
  conformal_at f x → conformal_at g (f x) → conformal_at (g ∘ f) x :=
begin
  rintro ⟨f', hf₁, cf, hcf, lief, hf₂⟩ ⟨g', hg₁, cg, hcg, lieg, hg₂⟩,
  -- ⟨ ⟩ can be used for `exists` too, no need for `use`
  exact ⟨g'.comp f', has_fderiv_at.comp x hg₁ hf₁, cg * cf, mul_ne_zero hcg hcf, lief.trans lieg,
  -- let `simp` do all the work. You don't need `simp only` if you can close the goal.
    by {ext, simp [coe_comp' f' g', hf₂, hg₂, smul_smul cg cf] }⟩,
end

theorem _root_.conformal_at_iff {f : X → Y} {x : X} {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) :
conformal_at f x ↔ ∃ (c : ℝ) (hc : c > 0), ∀ (u v : X), inner (f' u) (f' v) = (c : ℝ) * (inner u v) :=
begin
  split,
  { -- intros + rcases = rintros
    rintros ⟨f₁, h₁, c₁, hc₁, lie, h₂⟩,
    -- `use` and `intros` can be put together with `refine`. Note: also use `c₁ * c₁` not `c₁^2`, then you don't need `pow_two` later.
    refine ⟨c₁ * c₁, mul_self_pos hc₁, λ u v, _⟩,
    -- dot notation `f'.coe_coe` is much more brief than `continuous_linear_equiv.coe_coe f'`
    -- Also -- make `simp` do the work. You don't need to rewrite and then simp; simp does rewrites for you.
    simp [← f'.coe_coe, ← f'.coe_def_rev, has_fderiv_at.unique h h₁, h₂, inner_map_map, real_inner_smul_left,
      real_inner_smul_right, mul_assoc] },
  {rintro ⟨c₁, hc₁, huv⟩,
    let c := real.sqrt c₁⁻¹,
    have hc : c ≠ 0 := λ w, by {simp only [c] at w;
      exact (real.sqrt_ne_zero'.mpr $ inv_pos.mpr hc₁) w},
    let c_map := linear_equiv.smul_of_ne_zero ℝ Y c hc,
    let f₁ := f'.to_linear_equiv.trans c_map,
    have minor : ⇑f₁ = (λ (y : Y), c • y) ∘ f' := rfl,
    have minor' : ⇑f' = (λ (y : Y), c⁻¹ • y) ∘ f₁ := by ext;
      rw [minor, function.comp_apply, function.comp_apply,
          smul_smul, inv_mul_cancel hc, one_smul],
    have key : ∀ (u v : X), inner (f₁ u) (f₁ v) = inner u v := λ u v, by
      rw [minor, function.comp_app, function.comp_app, real_inner_smul_left,
          real_inner_smul_right, huv u v, ← mul_assoc, ← mul_assoc,
          real.mul_self_sqrt $ le_of_lt $ inv_pos.mpr hc₁,
          inv_mul_cancel $ ne_of_gt hc₁, one_mul],
    exact ⟨f'.to_continuous_linear_map, ⟨h, c⁻¹, inv_ne_zero hc, f₁.isometry_of_inner key, minor'⟩⟩,
  },
end

def char_fun {f : X → Y} (x : X) {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) (H : conformal_at f x) : ℝ :=
by choose c hc huv using (conformal_at_iff h).mp H; exact c

theorem _root_.conformal_at_preserves_angle {f : X → Y} {x : X} {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) (H : conformal_at f x) (u v : X) :
  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
begin
  -- don't begin a proof with `intros u v`, just put them before the colon
  repeat {rw inner_product_geometry.angle},
  suffices new : inner (f' u) (f' v) / (∥f' u∥ * ∥f' v∥) = inner u v / (∥u∥ * ∥v∥),
  { rw new, },
  {
    rcases H with ⟨f₁, h₁, c₁, hc₁, lie, h₂⟩,
    have minor : ∥c₁∥ ≠ 0 := λ w, hc₁ (norm_eq_zero.mp w),
    have : f'.to_continuous_linear_map = f₁ := has_fderiv_at.unique h h₁,
    rw [← continuous_linear_equiv.coe_coe f', ← continuous_linear_equiv.coe_def_rev f'],
    repeat {rw inner_product_angle.def},
    rw [this, h₂],
    repeat {rw function.comp_apply},
    rw [real_inner_smul_left, real_inner_smul_right, ← mul_assoc, linear_isometry_equiv.inner_map_map],
    repeat {rw [norm_smul, linear_isometry_equiv.norm_map]},
    rw [← mul_assoc],
    exact calc c₁ * c₁ * inner u v / (∥c₁∥ * ∥u∥ * ∥c₁∥ * ∥v∥)
            = c₁ * c₁ * inner u v / (∥c₁∥ * ∥c₁∥ * ∥u∥ * ∥v∥) : by simp only [mul_comm, mul_assoc]
        ... = c₁ * c₁ * inner u v / (abs c₁ * abs c₁ * ∥u∥ * ∥v∥) : by rw [real.norm_eq_abs]
        ... = c₁ * c₁ * inner u v / (c₁ * c₁ * ∥u∥ * ∥v∥) : by rw [← pow_two, ← sq_abs, pow_two]
        ... = c₁ * (c₁ * inner u v) / (c₁ * (c₁ * (∥u∥ * ∥v∥))) : by simp only [mul_assoc]
        ... = (c₁ * inner u v) / (c₁ * (∥u∥ * ∥v∥)) : by rw mul_div_mul_left _ _ hc₁
        ... = inner u v / (∥u∥ * ∥v∥) : by rw mul_div_mul_left _ _ hc₁,
  },
end

end conformal_at

def conformal
{X Y : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y]
(f : X → Y) := ∀ (x : X), conformal_at f x

namespace conformal

variables {X Y Z : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y] [inner_product_space ℝ Z]

theorem differentiable {f : X → Y} (h : conformal f) :
differentiable ℝ f := λ x, (h x).differentiable_at

theorem id : conformal (id : X → X) := λ x, conformal_at.id x

theorem const_smul {c : ℝ} (h : c ≠ 0) :
conformal (λ (x : X), c • x) := λ x, conformal_at.const_smul h x

theorem comp {f : X → Y} {g : Y → Z} (hf : conformal f) (hg : conformal g) :
conformal (g ∘ f) := λ x, conformal_at.comp (hf x) (hg (f x))

end conformal

end conformal_API

[Oliver Nash]

You might be surprised at how much dicussion just a few lines of new code can generate when under review so the smaller the PR, the better. As I say, I have only glanced but this much looks like a possible first PR.

[Kevin Buzzard]

The way dot notation works is that if f' has type X ≃L[ℝ] Y then of course this is just notation, and f' really has type continuous_linear_equiv blah blah blah... so f'.coe_coe is shorthand for continuous_linear_equiv.coe_coe f'.

[Kevin Buzzard]

Oh cool, Oliver's suggestion is pretty much exactly what I just read through :-) Consider that to be your first review!

[Yourong Zang]

Kevin Buzzard said:

I played with some of the first 150 lines. Your code is really good! In the comments below I show you some more tips.

import tactic
import data.matrix.notation
import analysis.complex.basic
import geometry.manifold.charted_space
import analysis.normed_space.inner_product
import linear_algebra.matrix.to_linear_equiv
import geometry.euclidean.basic
import analysis.complex.isometry
import analysis.normed_space.finite_dimension

noncomputable theory

-- I personally like to have section names which are "obviously not namespaces"
-- so that when I see `end conformal_API` I will know it's not the end of a namespace

section conformal_API

def is_conformal_map {X Y : Type*}
[inner_product_space ℝ X] [inner_product_space ℝ Y] (f' : X →L[ℝ] Y) :=
∃ (c : ℝ) (hc : c ≠ 0) (lie : X ≃ₗᵢ[ℝ] Y), ⇑f' = (λ y, c • y) ∘ lie

def conformal_at
{X Y : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y]
(f : X → Y) (x : X) :=
∃ (f' : X →L[ℝ] Y), has_fderiv_at f f' x ∧ is_conformal_map f'

-- let's make an API for `conformal_at` before we start on `conformal`.
-- Let's do it in a namespace and set up variables for that namespace.

namespace conformal_at

variables {X Y Z : Type*}
  [inner_product_space ℝ X] [inner_product_space ℝ Y] [inner_product_space ℝ Z]

-- save some time by opening these
open linear_isometry_equiv continuous_linear_map

theorem differentiable_at {f : X → Y} {x : X} (h : conformal_at f x) :
differentiable_at ℝ f x := let ⟨_, h₁, _, _, _, _⟩ := h in h₁.differentiable_at

-- I can use `refl` now instead of `linear_isometry_equiv.refl`
theorem id (x : X) : conformal_at id x :=
⟨id ℝ X, has_fderiv_at_id _, 1, one_ne_zero, refl ℝ X, by ext; simp⟩

theorem const_smul {c : ℝ} (h : c ≠ 0) (x : X) : conformal_at (λ (x': X), c • x') x :=
-- no `by apply` needed
⟨c • continuous_linear_map.id ℝ X, has_fderiv_at.const_smul (has_fderiv_at_id x) c, c, h, refl ℝ X, by ext; simp⟩

-- putting conformal_at f x before the colon means you can `rintro` everything
theorem comp {f : X → Y} {g : Y → Z} {x : X} :
  conformal_at f x → conformal_at g (f x) → conformal_at (g ∘ f) x :=
begin
  rintro ⟨f', hf₁, cf, hcf, lief, hf₂⟩ ⟨g', hg₁, cg, hcg, lieg, hg₂⟩,
  -- ⟨ ⟩ can be used for `exists` too, no need for `use`
  exact ⟨g'.comp f', has_fderiv_at.comp x hg₁ hf₁, cg * cf, mul_ne_zero hcg hcf, lief.trans lieg,
  -- let `simp` do all the work. You don't need `simp only` if you can close the goal.
    by {ext, simp [coe_comp' f' g', hf₂, hg₂, smul_smul cg cf] }⟩,
end

theorem _root_.conformal_at_iff {f : X → Y} {x : X} {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) :
conformal_at f x ↔ ∃ (c : ℝ) (hc : c > 0), ∀ (u v : X), inner (f' u) (f' v) = (c : ℝ) * (inner u v) :=
begin
  split,
  { -- intros + rcases = rintros
    rintros ⟨f₁, h₁, c₁, hc₁, lie, h₂⟩,
    -- `use` and `intros` can be put together with `refine`. Note: also use `c₁ * c₁` not `c₁^2`, then you don't need `pow_two` later.
    refine ⟨c₁ * c₁, mul_self_pos hc₁, λ u v, _⟩,
    -- dot notation `f'.coe_coe` is much more brief than `continuous_linear_equiv.coe_coe f'`
    -- Also -- make `simp` do the work. You don't need to rewrite and then simp; simp does rewrites for you.
    simp [← f'.coe_coe, ← f'.coe_def_rev, has_fderiv_at.unique h h₁, h₂, inner_map_map, real_inner_smul_left,
      real_inner_smul_right, mul_assoc] },
  {rintro ⟨c₁, hc₁, huv⟩,
    let c := real.sqrt c₁⁻¹,
    have hc : c ≠ 0 := λ w, by {simp only [c] at w;
      exact (real.sqrt_ne_zero'.mpr $ inv_pos.mpr hc₁) w},
    let c_map := linear_equiv.smul_of_ne_zero ℝ Y c hc,
    let f₁ := f'.to_linear_equiv.trans c_map,
    have minor : ⇑f₁ = (λ (y : Y), c • y) ∘ f' := rfl,
    have minor' : ⇑f' = (λ (y : Y), c⁻¹ • y) ∘ f₁ := by ext;
      rw [minor, function.comp_apply, function.comp_apply,
          smul_smul, inv_mul_cancel hc, one_smul],
    have key : ∀ (u v : X), inner (f₁ u) (f₁ v) = inner u v := λ u v, by
      rw [minor, function.comp_app, function.comp_app, real_inner_smul_left,
          real_inner_smul_right, huv u v, ← mul_assoc, ← mul_assoc,
          real.mul_self_sqrt $ le_of_lt $ inv_pos.mpr hc₁,
          inv_mul_cancel $ ne_of_gt hc₁, one_mul],
    exact ⟨f'.to_continuous_linear_map, ⟨h, c⁻¹, inv_ne_zero hc, f₁.isometry_of_inner key, minor'⟩⟩,
  },
end

def char_fun {f : X → Y} (x : X) {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) (H : conformal_at f x) : ℝ :=
by choose c hc huv using (conformal_at_iff h).mp H; exact c

theorem _root_.conformal_at_preserves_angle {f : X → Y} {x : X} {f' : X ≃L[ℝ] Y}
(h : has_fderiv_at f f'.to_continuous_linear_map x) (H : conformal_at f x) (u v : X) :
  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
begin
  -- don't begin a proof with `intros u v`, just put them before the colon
  repeat {rw inner_product_geometry.angle},
  suffices new : inner (f' u) (f' v) / (∥f' u∥ * ∥f' v∥) = inner u v / (∥u∥ * ∥v∥),
  { rw new, },
  {
    rcases H with ⟨f₁, h₁, c₁, hc₁, lie, h₂⟩,
    have minor : ∥c₁∥ ≠ 0 := λ w, hc₁ (norm_eq_zero.mp w),
    have : f'.to_continuous_linear_map = f₁ := has_fderiv_at.unique h h₁,
    rw [← continuous_linear_equiv.coe_coe f', ← continuous_linear_equiv.coe_def_rev f'],
    repeat {rw inner_product_angle.def},
    rw [this, h₂],
    repeat {rw function.comp_apply},
    rw [real_inner_smul_left, real_inner_smul_right, ← mul_assoc, linear_isometry_equiv.inner_map_map],
    repeat {rw [norm_smul, linear_isometry_equiv.norm_map]},
    rw [← mul_assoc],
    exact calc c₁ * c₁ * inner u v / (∥c₁∥ * ∥u∥ * ∥c₁∥ * ∥v∥)
            = c₁ * c₁ * inner u v / (∥c₁∥ * ∥c₁∥ * ∥u∥ * ∥v∥) : by simp only [mul_comm, mul_assoc]
        ... = c₁ * c₁ * inner u v / (abs c₁ * abs c₁ * ∥u∥ * ∥v∥) : by rw [real.norm_eq_abs]
        ... = c₁ * c₁ * inner u v / (c₁ * c₁ * ∥u∥ * ∥v∥) : by rw [← pow_two, ← sq_abs, pow_two]
        ... = c₁ * (c₁ * inner u v) / (c₁ * (c₁ * (∥u∥ * ∥v∥))) : by simp only [mul_assoc]
        ... = (c₁ * inner u v) / (c₁ * (∥u∥ * ∥v∥)) : by rw mul_div_mul_left _ _ hc₁
        ... = inner u v / (∥u∥ * ∥v∥) : by rw mul_div_mul_left _ _ hc₁,
  },
end

end conformal_at

def conformal
{X Y : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y]
(f : X → Y) := ∀ (x : X), conformal_at f x

namespace conformal

variables {X Y Z : Type*} [inner_product_space ℝ X] [inner_product_space ℝ Y] [inner_product_space ℝ Z]

theorem differentiable {f : X → Y} (h : conformal f) :
differentiable ℝ f := λ x, (h x).differentiable_at

theorem id : conformal (id : X → X) := λ x, conformal_at.id x

theorem const_smul {c : ℝ} (h : c ≠ 0) :
conformal (λ (x : X), c • x) := λ x, conformal_at.const_smul h x

theorem comp {f : X → Y} {g : Y → Z} (hf : conformal f) (hg : conformal g) :
conformal (g ∘ f) := λ x, conformal_at.comp (hf x) (hg (f x))

end conformal

end conformal_API

Thank you for the comments! I will study them and adjust the rest of the file accordingly, especially not starting the proof with intros something.

[Kevin Buzzard]

You should perhaps just PR this directly to mathlib. Your github username is justadzr -- @maintainers can Yourong have PR access to non-master branches of mathlib?

[Kevin Buzzard]

If you make a PR you will get some more experts looking at it carefully, including people (unlike me!) who actually know something about the subject.

[Yourong Zang]

Kevin Buzzard said:

Oh cool, Oliver's suggestion is pretty much exactly what I just read through :-) Consider that to be your first review!

Great, I will cut the first section and turn it into a PR.

[Johan Commelin]

@Yourong Zang https://github.com/leanprover-community/mathlib/invitations

[Kevin Buzzard]

Making stuff a PR will not slow down your work, because you can make the PR and then make your own project have that specific branch of mathlib as a dependency rather than master. My understanding is that you might find it difficult to just switch directly to working directly on a branch of mathlib because for your work on Riemann surfaces you might need some tricky facts about holomorphic functions which are not yet there. But this conformal stuff looks to me to be directly ready for mathlib. Thanks a lot for writing it!

[Yourong Zang]

Kevin Buzzard said:

Making stuff a PR will not slow down your work, because you can make the PR and then make your own project have that specific branch of mathlib as a dependency rather than master. My understanding is that you might find it difficult to just switch directly to working directly on a branch of mathlib because for your work on Riemann surfaces you might need some tricky facts about holomorphic functions which are not yet there. But this conformal stuff looks to me to be directly ready for mathlib. Thanks a lot for writing it!

Thank you. But in which branch should I make this pull request?

[Johan Commelin]

git checkout -b new-conformal-map-branch will create a new branch for you

[Johan Commelin]

But you can also use the git interface in VScode.

[Johan Commelin]

@Yourong Zang there is a youtube video on how to make mathlib PRs. If you are unfamiliar with git/github/PRs, you might want to watch it.

[Johan Commelin]

#howtoPR

[Yourong Zang]

Johan Commelin said:

Yourong Zang there is a youtube video on how to make mathlib PRs. If you are unfamiliar with git/github/PRs, you might want to watch it.

That is extremely helpful. Thank you!

[Patrick Massot]

This is very nice but I still think it's much more standard to ask that conformal linear maps are positive multiples of isometries.

[Kevin Buzzard]

Possibly stupid question alert: isn't multiplication by -1 an isometry, so it doesn't matter?

[Patrick Massot]

Right, I guess I meant you should add that they are orientation preserving.

[Yourong Zang]

Patrick Massot said:

Right, I guess I meant you should add that they are orientation preserving.

But wouldn't that exclude inversions in spaces of odd dimensions?

[Patrick Massot]

It's true this is weird. But anti-holomorphic map in complex dimension 1 should be anti-conformal, not conformal.

[Patrick Massot]

But that's not super important, especially since we are used to having more general definitions in formalization.

[Patrick Massot]

We should at least have a big warning in the relevant docstrings.

[Yourong Zang]

Patrick Massot said:

It's true this is weird. But anti-holomorphic map in complex dimension 1 should be anti-conformal, not conformal.

Then should I PR a file with the orientation-preserving definition?

[Patrick Massot]

I think you can keep your definition as long as you put a warning in the docstrings (at module and declaration levels).

[Patrick Massot]

Style remark: in mathlib we never put a brace alone on its line. See https://leanprover-community.github.io/contribute/style.html. Also, you should never need to type ⇑

[Yourong Zang]

Patrick Massot said:

I think you can keep your definition as long as you put a warning in the docstrings (at module and declaration levels).

Would it be better to just call these maps angle-preserving instead of conformal?

[Yourong Zang]

Patrick Massot said:

Style remark: in mathlib we never put a brace alone on its line. See https://leanprover-community.github.io/contribute/style.html. Also, you should never need to type ⇑

Thank you for the information. I will adjust the code.

[Patrick Massot]

angle-preserving is also ambiguous since it could mean either oriented or unoriented angles. And writing unoriented_angle_preserving would be too long.

[Yourong Zang]

Patrick Massot said:

angle-preserving is also ambiguous since it could mean either oriented or unoriented angles. And writing unoriented_angle_preserving would be too long.

Ok then I will put a warning in the docstrings.

[Yourong Zang]

Patrick Massot said:

angle-preserving is also ambiguous since it could mean either oriented or unoriented angles. And writing unoriented_angle_preserving would be too long.

Thank you for the instructions! They are extremely helpful.

[Kalle Kytölä]

Just wanted to say that I am also very excited to hear conformal maps are now on their way to mathlib, thanks to @Yourong Zang! :tada: :globe:

[Yourong Zang]

Thank you! Though the maps are not defined in the most general sense.

Kalle Kytölä said:

Just wanted to say that I am also very excited to hear conformal maps are now on their way to mathlib, thanks to Yourong Zang! :tada: :globe:

[Heather Macbeth]

Yourong Zang said:

Also, do we need partial derivatives to formalize Liouville's theorem on C^4 conformal mappings between Euclidean spaces?

Thanks for the PR, @Yourong Zang! In answer to this question -- you can use docs#times_cont_diff, letting n be 4, or just requiring 4 ≤ n.

[Yourong Zang]

Heather Macbeth said:

Yourong Zang said:

Also, do we need partial derivatives to formalize Liouville's theorem on C^4 conformal mappings between Euclidean spaces?

Thanks for the PR, Yourong Zang! In answer to this question -- you can use docs#times_cont_diff, letting n be 4, or just requiring 4 ≤ n.

Thank you for the comments. I didn't see anything about partial derivatives in mathlib/Zulip. Should I define them like fderiv \R f x (v i) for some standard basis v of a Euclidean space?

[Heather Macbeth]

I don't think that it's really necessary to work with a basis -- can you try to give a more abstract version of the argument that doesn't require it?

[Yourong Zang]

Heather Macbeth said:

I don't think that it's really necessary to work with a basis -- can you try to give a more abstract version of the argument that doesn't require it?

Unfortunately I am not sure about that. The materials I could find are quite limited, and most of them involve dealing with partial derivatives or Jacobians.

[Heather Macbeth]

Which source are you following? I can try to suggest a route to a more abstract argument.

[Yourong Zang]

Heather Macbeth said:

Which source are you following? I can try to suggest a route to a more abstract argument.

That would be wonderful and extremely helpful! I am currently searching for different proofs online to resolve the problem.