OAI/Analysis/Brenier/CellDerivative.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.hasDerivAt_positive_cell_cut_remainder line 21

   Source documentation

   The signed variation of one interface of a positive-mass affine cell. Compactness, convexity, injectivity, and positive cell masses now discharge all analytic bounds and all exceptional-face hypotheses. Other cuts may move independently, as required by the finite-intersection telescoping formula.

   theorem hasDerivAt_positive_cell_cut_remainder
       {d : ℕ} {ι : Type*} [Fintype ι]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
       (hpos : ∀ k, ρ (CellGeometry.closedCell K y c k) ≠ 0)
       {i j : ι} (hij : i ≠ j) {z : E d} (hz : z ∈ interior K)
       (htie : ⟪z, y i⟫_ℝ + c i = ⟪z, y j⟫_ℝ + c j)
       (w : E d → ℝ) (hw : Continuous w) (v : E d) (r : ℝ)
       (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
       (ell : ℝ → ι → E d → ℝ)
       (hell : ∀ k ∈ J, Continuous (fun p : ℝ × E d => ell p.1 k p.2))
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

2. lemma OAI.Problem358.PositiveCellFullDerivative.prod_sub_prod_ordered line 102
3. lemma OAI.Problem358.PositiveCellFullDerivative.cutIndicator_eq_ite line 135
4. lemma OAI.Problem358.PositiveCellFullDerivative.norm_cutIndicator_sub_le_one line 139
5. theorem OAI.Problem358.PositiveCellFullDerivative.hasDerivAt_cut_product_integral line 146

   Source documentation

   Ordered single-cut derivatives reassemble into the actual product integral. The order is used only for the proof, not in the resulting derivative.

   theorem hasDerivAt_cut_product_integral
       {ι X : Type*} [LinearOrder ι] [MeasurableSpace X]
       {μ : Measure X} (s : Finset ι) (ell : ℝ → ι → X → ℝ)
       (hell : ∀ t j, Measurable (ell t j))
       {w : X → ℝ} (hw : Integrable w μ) (D : ι → ℝ)
       (hd : ∀ j ∈ s, HasDerivAt (fun t : ℝ => ∫ x,
         (w x * ∏ k ∈ s.erase j,
           cutIndicator (if k < j then ell t k x else ell 0 k x)) *
             (cutIndicator (ell t j x) - cutIndicator (ell 0 j x)) ∂μ) (D j) 0) :
       HasDerivAt (fun t : ℝ => ∫ x,
         w x * ∏ j ∈ s, cutIndicator (ell t j x) ∂μ) (∑ j ∈ s, D j) 0 := by
   …

6. lemma OAI.Problem358.PositiveCellFullDerivative.prod_cutIndicator_eq_indicator line 201
7. def OAI.Problem358.PositiveCellFullDerivative.faceVariation line 218

   Source documentation

   The signed face integral in a full affine-cell variation.

   def faceVariation {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
       (K : Set (E d)) (y v : ι → E d) (c r : ι → ℝ)
       (w : E d → ℝ) (i j : ι) (z : E d) : ℝ :=
   …

8. theorem OAI.Problem358.PositiveCellFullDerivative.hasDerivAt_closedCell_integral line 230

   Source documentation

   Full scalar weighted-cell derivative. Only actual compact convex positive-cell geometry is assumed: all trace, domination, and signed-cut limits are proved.

   theorem hasDerivAt_closedCell_integral
       {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (y v : ι → E d) (c r : ι → ℝ) (hy : Function.Injective y)
       (hpos : ∀ k, ρ (CellGeometry.closedCell K y c k) ≠ 0)
       (w : E d → ℝ) (hw : Continuous w) (i : ι) (z : ι → E d)
       (hz : ∀ j, j ≠ i → z j ∈ interior K)
       (htie : ∀ j, j ≠ i → ⟪z j, y i⟫_ℝ + c i = ⟪z j, y j⟫_ℝ + c j) :
       HasDerivAt (fun t : ℝ => ∫ x in
         CellGeometry.closedCell K (fun j => y j + t • v j) (fun j => c j + t * r j) i,
         w x)
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

9. theorem OAI.Problem358.PositiveCellFullDerivative.hasDerivAt_uniform_closedCell_moment line 355

   Source documentation

   The genuine vector first-moment derivative, written in coordinates of the signed intrinsic face integrals. All scalar differentiation hypotheses are discharged by the full-cell calculus.

   theorem hasDerivAt_uniform_closedCell_moment
       {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (y v : ι → E d) (c r : ι → ℝ) (hy : Function.Injective y)
       (hpos : ∀ k, ρ (CellGeometry.closedCell K y c k) ≠ 0)
       (i : ι) (z : ι → E d)
       (hz : ∀ j, j ≠ i → z j ∈ interior K)
       (htie : ∀ j, j ≠ i → ⟪z j, y i⟫_ℝ + c i = ⟪z j, y j⟫_ℝ + c j) :
       HasDerivAt (fun t : ℝ => ∫ x in
         CellGeometry.closedCell K (fun j => y j + t • v j) (fun j => c j + t * r j) i,
         x ∂uniformMeasure K)
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

10. theorem OAI.Problem358.PositiveCellFullDerivative.hasDerivAt_uniform_closedCell_mass line 377

    Source documentation

    The true real mass derivative of a positive cell under the probability source, with normalization by the source volume.

    theorem hasDerivAt_uniform_closedCell_mass
        {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
        (y v : ι → E d) (c r : ι → ℝ) (hy : Function.Injective y)
        (hpos : ∀ k, ρ (CellGeometry.closedCell K y c k) ≠ 0)
        (i : ι) (z : ι → E d)
        (hz : ∀ j, j ≠ i → z j ∈ interior K)
        (htie : ∀ j, j ≠ i → ⟪z j, y i⟫_ℝ + c i = ⟪z j, y j⟫_ℝ + c j) :
        HasDerivAt (fun t : ℝ => (uniformMeasure K).real
          (CellGeometry.closedCell K (fun j => y j + t • v j) (fun j => c j + t * r j) i))
          ((∑ j ∈ Finset.univ.erase i, faceVariation K y v c r (fun _ => 1) i j (z j)) /
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.PositiveCellFullDerivative.faceVariation