BranchDensity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.integral_sq_eq_one_of_densityMeasure_probability line 14

Source documentation

Probability of a square density gives its ordinary integral normalization.

theorem integral_sq_eq_one_of_densityMeasure_probability
    {g : E3 → ℝ} (hg : Measurable g)
    [IsProbabilityMeasure (densityMeasure (fun x => (g x) ^ 2))] :
    (∫ x : E3, (g x) ^ 2 ∂(volume : Measure E3)) = 1 := by
…

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

theorem OAI.Problem356.isProbabilityMeasure_densityMeasure_unit_sq line 27

Source documentation

A smooth compact unit square defines a probability measure.

theorem isProbabilityMeasure_densityMeasure_unit_sq
    {g : E3 → ℝ}
    (hsm : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g)
    (hcs : HasCompactSupport g)
    (hmass : (∫ x : E3, (g x) ^ 2 ∂(volume : Measure E3)) = 1) :
    IsProbabilityMeasure (densityMeasure (fun x => (g x) ^ 2)) := by
…

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

def OAI.Problem356.branchDensityWeight line 46
Source documentation
The weights of the central and four outer squares.
```
def branchDensityWeight (i : Fin 5) : ℝ := if i = 0 then 1 / 3 else 1 / 6
```
lemma OAI.Problem356.branchDensityWeight_nonneg line 48
lemma OAI.Problem356.sum_branchDensityWeight line 52

theorem OAI.Problem356.exists_smooth_density_eq_branchMarginal line 57

Source documentation

Five disjoint square amplitudes, with the four outer square laws obtained by the prescribed branch pushforwards, form the exact smooth branch marginal.

theorem exists_smooth_density_eq_branchMarginal
    (g : Fin 5 → E3 → ℝ) (H : Fin 4 → E3 → E3)
    (hgn : ∀ i x, 0 ≤ g i x)
    (hgs : ∀ i, ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) (g i))
    (hgc : ∀ i, HasCompactSupport (g i))
    (hgd : Pairwise fun i j =>
      Disjoint (Function.support (g i)) (Function.support (g j)))
    (hzero : (∫ x : E3, (g 0 x) ^ 2 ∂(volume : Measure E3)) = 1)
    (hH : ∀ i, Measurable (H i))
    (hmap : ∀ i : Fin 4,
      densityMeasure (fun x => (g i.succ x) ^ 2) =
        Measure.map (H i) (densityMeasure (fun x => (g 0 x) ^ 2))) :
…

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