OAI/Analysis/Brenier/CutDerivative.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.AffineHalfspaceSpeed.speed line 16

   Source documentation

   The normal velocity of an affine cut, in a fixed transverse coordinate.

   def speed (n u v : V) (r h : ℝ) (x : V) : ℝ :=
   …

2. theorem OAI.Problem358.AffineHalfspaceSpeed.perturbed_affine_eq line 19
3. theorem OAI.Problem358.AffineHalfspaceSpeed.perturbed_nonneg_iff line 28

   Source documentation

   A tilted affine inequality is an exact moving scalar threshold.

   theorem perturbed_nonneg_iff (n u v x : V) (c r h t : ℝ)
       (hface : ⟪n, x⟫_ℝ + c = 0)
       (hden : 0 < ⟪n, u⟫_ℝ + h * ⟪v, u⟫_ℝ) :
       0 ≤ ⟪n + h • v, x + t • u⟫_ℝ + (c + h * r) ↔
         -h * speed n u v r h x ≤ t := by
   …

   Mentions: OAI.Problem358.AffineHalfspaceSpeed.speed

4. theorem OAI.Problem358.AffineHalfspaceSpeed.base_nonneg_iff line 39

   Source documentation

   The unperturbed cut is the zero threshold.

   theorem base_nonneg_iff (n u x : V) (c t : ℝ)
       (hface : ⟪n, x⟫_ℝ + c = 0) (htrans : 0 < ⟪n, u⟫_ℝ) :
       0 ≤ ⟪n, x + t • u⟫_ℝ + c ↔ 0 ≤ t := by
   …

5. theorem OAI.Problem358.AffineHalfspaceSpeed.eventually_denominator_half line 45

   Source documentation

   The transverse denominator stays uniformly above half its initial value.

   theorem eventually_denominator_half (n u v : V) (htrans : 0 < ⟪n, u⟫_ℝ) :
       ∀ᶠ h : ℝ in 𝓝 0, ⟪n, u⟫_ℝ / 2 < ⟪n, u⟫_ℝ + h * ⟪v, u⟫_ℝ := by
   …

6. theorem OAI.Problem358.AffineHalfspaceSpeed.continuousAt_speed line 53
7. theorem OAI.Problem358.AffineHalfspaceSpeed.tendsto_speed line 60
8. theorem OAI.Problem358.AffineHalfspaceSpeed.abs_speed_le line 67

   Source documentation

   A uniform speed bound on a bounded subset of the reference face.

   theorem abs_speed_le (n u v : V) (r h R : ℝ) (x : V)
       (htrans : 0 < ⟪n, u⟫_ℝ)
       (hden : ⟪n, u⟫_ℝ / 2 ≤ ⟪n, u⟫_ℝ + h * ⟪v, u⟫_ℝ)
       (hx : ‖x‖ ≤ R) :
       |speed n u v r h x| ≤ 2 * (|r| + ‖v‖ * R) / ⟪n, u⟫_ℝ := by
   …

   Mentions: OAI.Problem358.AffineHalfspaceSpeed.speed

9. theorem OAI.Problem358.AffineHalfspaceSpeed.eventually_abs_speed_le line 89

   Source documentation

   The bound is simultaneous over the whole bounded face region.

   theorem eventually_abs_speed_le (n u v : V) (r R : ℝ)
       (htrans : 0 < ⟪n, u⟫_ℝ) :
       ∀ᶠ h : ℝ in 𝓝 0, ∀ x : V, ‖x‖ ≤ R →
         |speed n u v r h x| ≤ 2 * (|r| + ‖v‖ * R) / ⟪n, u⟫_ℝ := by
   …

   Mentions: OAI.Problem358.AffineHalfspaceSpeed.speed

10. theorem OAI.Problem358.AffineHalfspaceSpeed.tendsto_scaled_point line 97

    Source documentation

    Points in the rescaled moving strip converge to their reference-face point.

    theorem tendsto_scaled_point (n u v x : V) (r a : ℝ)
        (htrans : ⟪n, u⟫_ℝ ≠ 0) :
        Tendsto (fun h : ℝ => x + (-h * speed n u v r h x * a) • u)
          (𝓝 0) (𝓝 x) := by
    …

    Mentions: OAI.Problem358.AffineHalfspaceSpeed.speed

11. theorem OAI.Problem358.AffineHalfspaceSpeed.measurable_speed line 112

    Source documentation

    Joint measurability remains valid even where the totalized denominator vanishes.

    theorem measurable_speed (n u v : V) (r : ℝ) :
        Measurable (fun p : ℝ × V => speed n u v r p.1 p.2) := by
    …

    Mentions: OAI.Problem358.AffineHalfspaceSpeed.speed

12. theorem OAI.Problem358.AffineHalfspaceSpeed.measurable_scaled_point line 117
13. theorem OAI.Problem358.hasDerivAt_integral_affine_cut_difference line 136

    Source documentation

    Differentiation of an actual moving affine cut in a fixed transverse chart. The affine threshold identity, local denominator bounds, velocity limit, and velocity measurability are all consequences, not extra hypotheses.

    theorem hasDerivAt_integral_affine_cut_difference
        {X V : Type*} [MeasurableSpace X]
        [NormedAddCommGroup V] [InnerProductSpace ℝ V]
        [MeasurableSpace V] [BorelSpace V]
        {μ : Measure X} [SFinite μ] {ρ : Measure V}
        (base : X → V) (hbase : Measurable base) (n u v : V) (c r : ℝ)
        (hchart : MeasurePreserving
          (fun p : X × ℝ => base p.1 + p.2 • u) (μ.prod volume) ρ)
        (hface : ∀ x, ⟪n, base x⟫_ℝ + c = 0)
        (htrans : 0 < ⟪n, u⟫_ℝ)
        {f : ℝ → V → ℝ} (hf : ∀ h, Measurable (f h))
        (B trace : X → ℝ)
    …

14. theorem OAI.Problem358.hasDerivAt_compact_affine_cut_remainder line 214

    Source documentation

    A compact source and an almost-everywhere regular reference face suffice to differentiate a moving cut with all other moving cut indicators attached. In particular, the trace limit, compact domination, ambient integrability, affine velocity, and exact threshold identity are all proved internally.

    theorem hasDerivAt_compact_affine_cut_remainder
        {ι X V : Type*} [TopologicalSpace X] [MeasurableSpace X]
        [OpensMeasurableSpace X] [T2Space X]
        [NormedAddCommGroup V] [InnerProductSpace ℝ V]
        [MeasurableSpace V] [BorelSpace V]
        {μ : Measure X} [SFinite μ] [IsFiniteMeasureOnCompacts μ]
        {ρ : Measure V} [IsFiniteMeasureOnCompacts ρ]
        {K : Set V} (hK : IsCompact K) (w : V → ℝ) (hw : Continuous w)
        (base : X → V) (hbase : Continuous base) (n u v : V) (c r : ℝ)
        (hchart : MeasurePreserving
          (fun p : X × ℝ => base p.1 + p.2 • u) (μ.prod volume) ρ)
        (P : V → X) (hP : Continuous P)
    …