ExtendedPushforward.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Square-density transport through globally measurable extensions of local branches.

theorem OAI.Problem356.squareDensity_ae_mem_of_tsupport_subset line 15
Source documentation
A square density is concentrated on every measurable set containing the amplitude's support.
```
theorem squareDensity_ae_mem_of_tsupport_subset
    (g : E3 → ℝ) {U : Set E3} (hU : MeasurableSet U) (hg : tsupport g ⊆ U) :
    ∀ᵐ x ∂densityMeasure (fun x => g x ^ 2), x ∈ U := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure
theorem OAI.Problem356.map_extendedBranch_squareDensity line 28
Source documentation
Extending a local branch by a fixed value outside its source does not affect its transport of a square density supported strictly inside that source.
```
theorem map_extendedBranch_squareDensity
    (e : OpenPartialHomeomorph E3 E3) (z : E3) (g : E3 → ℝ)
    (hg : tsupport g ⊆ e.source) :
    Measure.map (LocalBranchMeasure.extendedBranch e z)
        (densityMeasure (fun x => g x ^ 2)) =
      Measure.map e (densityMeasure (fun x => g x ^ 2)) :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.LocalBranchMeasure.extendedBranch, OAI.Problem356.densityMeasure

theorem OAI.Problem356.map_squareDensity_extendedBranch line 38

Source documentation

The exact inverse-Jacobian pushforward formula for a globally Borel branch.

theorem map_squareDensity_extendedBranch
    (e : OpenPartialHomeomorph E3 E3) (z : 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 (LocalBranchMeasure.extendedBranch e z)
        (densityMeasure (fun x => g x ^ 2)) =
      densityMeasure (fun y =>
        localTransportAmplitude e g (fun t => Real.sqrt |(D t).det|) y ^ 2) := by
…

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