DCRegularity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MahlerStokes.contDiffAt_dcForm line 14
Source documentation
The normalized d^c form of a C2 real potential is C1.
```
theorem contDiffAt_dcForm {τ : E → ℝ} {x : E} (hτ : ContDiffAt ℝ 2 τ x) :
    ContDiffAt ℝ 1 (dcForm τ) x := by
…
```
Mentions: OAI.MahlerStokes.dcForm
theorem OAI.MahlerStokes.contDiffAt_dcForm_log line 23