OAI/Analysis/AffineBernstein/ProductEquator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.product_vertical_hyperplane_volume_zero line 16
  2. lemma OAI.AffineBernstein.product_sphere_equator_null line 26

    Source comment

    The equator is null for the actual Haar-induced sphere measure.
    lemma product_sphere_equator_null :
    (volume : Measure (WithLp 2 (F × ℝ))).toSphere
      {e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1 | (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 = 0} = 0 := by
…
  3. theorem OAI.AffineBernstein.product_sphere_lintegral_split line 43

    Source comment

    Full-sphere nonnegative integration is the sum of the two open hemispheres. The codimension-one null set is proved from product volume, including dim F=0.
    theorem product_sphere_lintegral_split (g : WithLp 2 (F × ℝ) → ℝ≥0∞)
    (hg : Measurable g) :
    (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1, g e ∂volume.toSphere) =
      (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1,
        if 0 < (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 then g e else 0 ∂volume.toSphere) +
      (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1,
        if (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 < 0 then g e else 0 ∂volume.toSphere) := by
…
  4. theorem OAI.AffineBernstein.product_sphere_negative_lintegral line 66

    Source comment

    Antipodal transport identifies the negative hemisphere with a positive one.
    theorem product_sphere_negative_lintegral (g : WithLp 2 (F × ℝ) → ℝ≥0∞) :
    (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1,
      if (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 < 0 then g e else 0 ∂volume.toSphere) =
    (∫⁻ e : Metric.sphere (0:WithLp 2 (F × ℝ)) 1,
      if 0 < (WithLp.ofLp (e:WithLp 2 (F × ℝ))).2 then g (- (e:WithLp 2 (F × ℝ)))
      else 0 ∂volume.toSphere) := by
…