OAI/Analysis/CoulombTransport/SmoothBranchMarginal.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.SmoothBranchMarginal.squareDensity_probability line 16
2. theorem OAI.Problem356.SmoothBranchMarginal.squareDensity_ae_tsupport line 31
3. theorem OAI.Problem356.SmoothBranchMarginal.square_integral_eq_one line 40
4. theorem OAI.Problem356.SmoothBranchMarginal.transported_square_amplitude line 52

   Source documentation

   A normalized smooth amplitude transports to another normalized smooth amplitude. The derivative and its smooth square-root determinant are explicit inputs, so the result is compatible with independently constructed local charts.

   theorem transported_square_amplitude
       (e : OpenPartialHomeomorph E3 E3) {g : E3 → ℝ}
       (hg0 : ∀ x, 0 ≤ g x)
       (hg : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g)
       (hgc : HasCompactSupport g) (hgs : tsupport g ⊆ e.source)
       (hmass : (∫ x : E3, g x ^ 2) = 1)
       (he : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e.symm e.target)
       (D : E3 → E3 →L[ℝ] E3)
       (hD : ∀ y ∈ e.target, HasFDerivAt e.symm (D y) y)
       (hJ : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
         (fun y => Real.sqrt |(D y).det|) e.target) :
       ∃ q : E3 → ℝ,
   …

   Mentions: OAI.Problem356.E3

5. def OAI.Problem356.SmoothBranchMarginal.componentWeight line 89

   Source documentation

   The five component weights are fixed by the counterexample construction.

   def componentWeight : Option (Fin 4) → ℝ
     | none => 1 / 3
     | some _ => 1 / 6

6. def OAI.Problem356.SmoothBranchMarginal.componentAmplitude line 93
7. def OAI.Problem356.SmoothBranchMarginal.componentRegion line 98
8. def OAI.Problem356.SmoothBranchMarginal.marginalDensity line 103
9. def OAI.Problem356.SmoothBranchMarginal.NormalizedAmplitude line 106
10. theorem OAI.Problem356.SmoothBranchMarginal.marginalDensity_smooth line 111
11. theorem OAI.Problem356.SmoothBranchMarginal.marginalDensity_measure line 147
12. theorem OAI.Problem356.SmoothBranchMarginal.exists_smooth_branch_marginal line 165

    Source documentation

    Construct the actual smooth five-component marginal from local branch charts on a common ball. All square amplitudes and their exact pushforward laws are supplied in the conclusion.

    theorem exists_smooth_branch_marginal
        (c : E3) {r : ℝ} (hr : 0 < r)
        (e : Fin 4 → OpenPartialHomeomorph E3 E3)
        (hsource : ∀ i, Metric.ball c r ⊆ (e i).source)
        (hdisj : Pairwise (fun i j => Disjoint
          (componentRegion (Metric.ball c r) e i) (componentRegion (Metric.ball c r) e j)))
        (he : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) (e i).symm (e i).target)
        (D : Fin 4 → E3 → E3 →L[ℝ] E3)
        (hD : ∀ i y, y ∈ (e i).target → HasFDerivAt (e i).symm (D i y) y)
        (hJ : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
          (fun y => Real.sqrt |(D i y).det|) (e i).target) :
        ∃ (g : E3 → ℝ) (q : Fin 4 → E3 → ℝ),
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.SmoothBranchMarginal.componentRegion

13. theorem OAI.Problem356.SmoothBranchMarginal.exists_smooth_branch_marginal_of_smooth_charts line 202

    Source documentation

    The preceding construction only needs smoothness in both directions of the local charts; no determinant or change-of-variables premise remains.

    theorem exists_smooth_branch_marginal_of_smooth_charts
        (c : E3) {r : ℝ} (hr : 0 < r)
        (e : Fin 4 → OpenPartialHomeomorph E3 E3)
        (hsource : ∀ i, Metric.ball c r ⊆ (e i).source)
        (hdisj : Pairwise (fun i j => Disjoint
          (componentRegion (Metric.ball c r) e i) (componentRegion (Metric.ball c r) e j)))
        (he : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) (e i) (e i).source)
        (he' : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) (e i).symm (e i).target) :
        ∃ (g : E3 → ℝ) (q : Fin 4 → E3 → ℝ),
          NormalizedAmplitude g ∧ tsupport g ⊆ Metric.ball c r ∧
          (∀ i, NormalizedAmplitude (q i) ∧ tsupport (q i) ⊆ e i '' Metric.ball c r) ∧
          IsProbabilityMeasure (densityMeasure (fun x => g x ^ 2)) ∧
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.SmoothBranchMarginal.componentRegion, OAI.Problem356.SmoothBranchMarginal.NormalizedAmplitude, OAI.Problem356.densityMeasure

14. structure OAI.Problem356.SmoothBranchMarginal.SmoothBranchData line 230

    Source documentation

    The construction data expected by the measure-level nonattainment and separated-support approximation arguments.

    structure SmoothBranchData (B : Set E3) where
    …

    Mentions: OAI.Problem356.E3

15. theorem OAI.Problem356.SmoothBranchMarginal.SmoothBranchData.central_full line 251
16. theorem OAI.Problem356.SmoothBranchMarginal.SmoothBranchData.central_disjoint line 254
17. theorem OAI.Problem356.SmoothBranchMarginal.SmoothBranchData.outer_disjoint line 258
18. theorem OAI.Problem356.SmoothBranchMarginal.SmoothBranchData.density_eq_four line 264

    Source documentation

    The explicit four-term form is definitionally the canonical branch marginal.

    theorem SmoothBranchData.density_eq_four {B : Set E3} (d : SmoothBranchData B) :
        densityMeasure d.rho = (1 / 3 : ℝ≥0∞) • d.nu + (1 / 6 : ℝ≥0∞) •
          (Measure.map (d.branch 0) d.nu + Measure.map (d.branch 1) d.nu +
            Measure.map (d.branch 2) d.nu + Measure.map (d.branch 3) d.nu) := by
    …

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

19. theorem OAI.Problem356.SmoothBranchMarginal.exists_smoothBranchData_of_smooth_charts line 274

    Source documentation

    A measure-level packaging of the actual smooth marginal construction. All branch extensions are globally measurable, while continuity is retained on the compact support where it is needed.

    theorem exists_smoothBranchData_of_smooth_charts
        (c : E3) {r : ℝ} (hr : 0 < r)
        (e : Fin 4 → OpenPartialHomeomorph E3 E3)
        (hsource : ∀ i, Metric.ball c r ⊆ (e i).source)
        (hdisj : Pairwise (fun i j => Disjoint
          (componentRegion (Metric.ball c r) e i) (componentRegion (Metric.ball c r) e j)))
        (he : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) (e i) (e i).source)
        (he' : ∀ i, ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) (e i).symm (e i).target) :
        ∃ d : SmoothBranchData (Metric.ball c r),
          ∀ i x, x ∈ Metric.ball c r → d.branch i x = e i x := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.SmoothBranchMarginal.componentRegion, OAI.Problem356.SmoothBranchMarginal.SmoothBranchData