PlaneHeatLaplacian.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cartesian integration by parts for the Euclidean Gaussian.

theorem OAI.ForcedComputation.PlaneHeat.integral_cartesian line 14
theorem OAI.ForcedComputation.PlaneHeat.integral_cartesian_symm line 23
theorem OAI.ForcedComputation.PlaneHeat.product_data_integrable line 32

theorem OAI.ForcedComputation.PlaneHeat.integral_second_one line 40

Source documentation

Integration by parts in the second Cartesian coordinate; hypotheses refer to the actual one-variable slices of the data.

theorem integral_second_one {t : ℝ} (ht : 0 < t) {f f' f'' : Plane → F}
    (hf : Continuous f) (hf'' : Continuous f'')
    (hd : ∀ r s, HasDerivAt (fun y => f ![r,y]) (f' ![r,s]) s)
    (hdd : ∀ r s, HasDerivAt (fun y => f' ![r,y]) (f'' ![r,s]) s)
    (C D E : ℝ) (hC : ∀ x, ‖f x‖ ≤ C) (hD : ∀ x, ‖f' x‖ ≤ D)
    (hE : ∀ x, ‖f'' x‖ ≤ E) :
    (∫ x : Plane, (oneDim t (x 0) * oneDimSecond t (x 1)) • f x) =
      ∫ x : Plane, kernel t x • f'' x := by
…

Mentions: OAI.ForcedComputation.PlaneHeat.oneDim, OAI.ForcedComputation.PlaneHeat.oneDimSecond, OAI.ForcedComputation.PlaneHeat.kernel

theorem OAI.ForcedComputation.PlaneHeat.integral_second_zero line 64