Complex Analysis, Naming Convention Woes

Stream: mathlib4

[Stefan Kebekus]

I would like to ask your help naming theorems in complex analysis. Specifically, I am struggling to find acceptable names for (many) variants of the classic mean value theorem for analytic and harmonic functions. At present, there are two main theorems in Mathlib.Analysis.Complex.MeanValue.

variable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ → E} {R : ℝ} {c : ℂ}

theorem circleAverage_of_differentiable_on
    (hf : ∀ z ∈ Metric.closedBall c |R|, DifferentiableAt ℂ f z) :
    Real.circleAverage f c R = f c :=
  by sorry

theorem circleAverage_sub_sub_inv_smul_of_differentiable_on
    (hf : ∀ z ∈ Metric.closedBall c |R|, DifferentiableAt ℂ f z)
    (hw : w ∈ Metric.ball c |R|) (hR : R ≠ 0) :
    Real.circleAverage (fun (z : ℂ) => ((z - c) / (z - w)) • f z) c R = f w :=
  by sorry

I am already a bit unsure if circleAverage_sub_sub_inv_smul_of_differentiable_on was a great choice. Soon, I would like to PR a variant (due to Poisson) with a real-valued kernel.

theorem circleAverage_of_differentiable_on_of_xxx
    (hf : DiffContOnCl ℂ f (ball c R)) (hw : w ∈ ball c R) :
    circleAverage (fun z ↦ ((z - c + (w - c)) / (z - w)).re • f z) c R = f w :=
  by sorry

More variants are in the pipeline. What would be a good naming scheme?

[Sébastien Gouëzel]

For your last statement, it should not mention differentiable_on but diffContOnCl. So, something like circleAverage_re_smul_of_diffContOnCl. Keep only in the theorem the main features of the lemma to distinguish between them. For me, the main point of the version you've written is that you're using a real part, so that's what I've kept in the name. Since you're writing the different versions, you know why you need them and what's important in them, so that's what you should mention in the name.

[Stefan Kebekus]

@Sébastien Gouëzel Thanks. Do you feel I should rename circleAverage_sub_sub_inv_smul_of_differentiable_on?

[Sébastien Gouëzel]

I'd say try to find names for your lemmas, and once you've found a naming scheme you're happy with you can consider renaming the other lemmas for coherence. A good idea would also be to fix the lemmas when their assumptions are too strong (as you've written, the correct assumption is DiffContOnCl, which is weaker than the current ∀ z ∈ Metric.closedBall c |R|, DifferentiableAt ℂ f z)

[Stefan Kebekus]

Thanks again, message taken. The rectification of the assumptions is already underway, in PR #35087.