SmoothPushforward.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.contDiff_of_contDiffOn_of_tsupport_subset line 15
Source documentation
A smooth function on an open set extends smoothly by zero whenever its closed support stays in that open set. The function is already defined on the ambient space; the support hypothesis expresses the extension.
```
theorem contDiff_of_contDiffOn_of_tsupport_subset
    {f : E3 → ℝ} {s : Set E3} {n : WithTop ENat}
    (hs : IsOpen s) (hf : ContDiffOn ℝ n f s) (hfs : tsupport f ⊆ s) :
    ContDiff ℝ n f := by
…
```
Mentions: OAI.Problem356.E3
def OAI.Problem356.localTransportAmplitude line 30
Source documentation
Transport of a compactly supported amplitude through a local homeomorphism, with a prescribed Jacobian square-root factor.
```
def localTransportAmplitude (e : OpenPartialHomeomorph E3 E3)
    (g J : E3 → ℝ) : E3 → ℝ :=
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.localTransportAmplitude_nonneg line 34
theorem OAI.Problem356.support_localTransportAmplitude_subset line 44
theorem OAI.Problem356.tsupport_localTransportAmplitude_subset line 57
theorem OAI.Problem356.hasCompactSupport_localTransportAmplitude line 64
theorem OAI.Problem356.tsupport_localTransportAmplitude_subset_target line 71
theorem OAI.Problem356.contDiff_localTransportAmplitude line 79

theorem OAI.Problem356.map_withDensity_localHomeomorph line 96

Source documentation

The inverse-Jacobian change-of-variables formula for a local homeomorphism. No global behavior outside its source is required.

theorem map_withDensity_localHomeomorph
    (e : OpenPartialHomeomorph E3 E3) (w : E3 → ℝ≥0∞)
    (D : E3 → E3 →L[ℝ] E3)
    (hD : ∀ y ∈ e.target, HasFDerivAt e.symm (D y) y) :
    Measure.map e (((volume : Measure E3).restrict e.source).withDensity w) =
      ((volume : Measure E3).restrict e.target).withDensity
        (fun y => ENNReal.ofReal |(D y).det| * w (e.symm y)) := by
…

Mentions: OAI.Problem356.E3

theorem OAI.Problem356.map_squareDensity_localHomeomorph line 132

Source documentation

The local inverse-Jacobian formula carries a square density to a square density, exactly as required by the five-component construction.

theorem map_squareDensity_localHomeomorph
    (e : OpenPartialHomeomorph E3 E3) (g : E3 → ℝ)
    (hgs : tsupport g ⊆ e.source)
    (D : E3 → E3 →L[ℝ] E3)
    (hD : ∀ y ∈ e.target, HasFDerivAt e.symm (D y) y) :
    Measure.map e (densityMeasure (fun x => g x ^ 2)) =
      densityMeasure (fun y =>
        localTransportAmplitude e g (fun z => Real.sqrt |(D z).det|) y ^ 2) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure, OAI.Problem356.localTransportAmplitude