Revision #1347 → #2597 · back to history
modifiedHarmonic functions1aa8bd4c426e
| Field | From #1347 | To #2597 |
|---|
| mathlib.decl | HarmonicAt | InnerProductSpace.HarmonicAt |
| provenance | ai | ai-moderated |
modifiedPrinciple of superposition5a09b15d9303
| Field | From #1347 | To #2597 |
|---|
| mathlib.decl | HarmonicOnNhd.add | InnerProductSpace.HarmonicOnNhd.add |
| provenance | ai | ai-moderated |
modifiedPoisson kernel formula on the disk8701ae420467
| Field | From #1347 | To #2597 |
|---|
| mathlib.decl | HarmonicContOnCl.circleAverage_poissonKernel_smul | InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul |
| provenance | ai | ai-moderated |
modifiedPoisson integral formula746b6c6ff75e
| Field | From #1347 | To #2597 |
|---|
| mathlib.decl | HarmonicContOnCl.circleAverage_poissonKernel_smul | InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul |
| provenance | ai | ai-moderated |