OAI/Analysis/CoulombTransport/Density.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.isSmoothCompactProbabilityDensity_sq line 14

   Source documentation

   A nonnegative smooth compactly supported square with mass one is an admissible density, including the extra square-root regularity.

   theorem isSmoothCompactProbabilityDensity_sq
       {g : E3 → ℝ}
       (hg_nonneg : ∀ x, 0 ≤ g x)
       (hg_smooth : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g)
       (hg_compact : HasCompactSupport g)
       (hg_mass : (∫ x : E3, (g x) ^ 2 ∂(volume : Measure E3)) = 1) :
       IsSmoothCompactProbabilityDensity (fun x => (g x) ^ 2) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.IsSmoothCompactProbabilityDensity

2. theorem OAI.Problem356.isSmoothCompactProbabilityDensity_normalized_sq line 30

   Source documentation

   Normalizing a nonnegative smooth square preserves smoothness of its square root.

   theorem isSmoothCompactProbabilityDensity_normalized_sq
       {g : E3 → ℝ}
       (hg_nonneg : ∀ x, 0 ≤ g x)
       (hg_smooth : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g)
       (hg_compact : HasCompactSupport g)
       (hg_mass_pos : 0 < ∫ x : E3, (g x) ^ 2 ∂(volume : Measure E3)) :
       IsSmoothCompactProbabilityDensity
         (fun x => (g x / Real.sqrt (∫ y : E3, (g y) ^ 2 ∂(volume : Measure E3))) ^ 2) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.IsSmoothCompactProbabilityDensity

3. theorem OAI.Problem356.exists_normalized_smooth_square_in_ball line 49

   Source documentation

   A normalized nonnegative smooth square can be placed in any positive-radius ball.

   theorem exists_normalized_smooth_square_in_ball (c : E3) {r : ℝ} (hr : 0 < r) :
       ∃ g : E3 → ℝ,
         (∀ x, 0 ≤ g x) ∧
         ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g ∧
         HasCompactSupport g ∧
         tsupport g ⊆ Metric.ball c r ∧
         (∫ x : E3, (g x) ^ 2 ∂(volume : Measure E3)) = 1 := by
   …

   Mentions: OAI.Problem356.E3