Theorems · Theorem · potential theory

InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq

∀ {f : ℂ → ℝ} {z : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.ball z R) →
    ∃ F, AnalyticOnNhd ℂ F (Metric.ball z R) ∧ Set.EqOn (fun z => (F z).re) f (Metric.ball z R)

Defined in: Mathlib.Analysis.Complex.Harmonic.Analytic
Cited by: 4 results in Mathlib
Foundations: Depth 287 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites67

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idproof · cited by 18,349
Complexstatement and proof · cited by 5,565
ContinuousLinearMapproof · cited by 5,352
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
zero_addproof · cited by 2,366
MulZeroClass.mul_zeroproof · cited by 2,091
Complex.ofRealproof · cited by 1,654
MulZeroClass.zero_mulproof · cited by 1,625
PseudoMetricSpaceproof · cited by 1,550

Cited by4

Results whose statement or proof uses this declaration.

InnerProductSpace.HarmonicOnNhd.circleAverage_eqproof · cited by 5
InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smulproof · cited by 2
HarmonicAt.analyticAtproof · cited by 0
harmonic_is_realOfHolomorphicproof · cited by 0