OAI/Analysis/Brenier/HalfspaceKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.stronglyMeasurable_intervalIntegral_endpoints line 13

   Source documentation

   Joint measurability is preserved by integrating between measurable endpoints.

   theorem stronglyMeasurable_intervalIntegral_endpoints
       {X : Type*} [MeasurableSpace X] {f : X → ℝ → ℝ} {a b : X → ℝ}
       (hf : Measurable (Function.uncurry f)) (ha : Measurable a) (hb : Measurable b) :
       StronglyMeasurable (fun x => ∫ t in a x..b x, f x t) := by
   …

2. theorem OAI.Problem358.hasDerivAt_integral_moving_boundary line 52

   Source documentation

   Differentiate a moving one-dimensional boundary, then integrate over the transverse variables. Continuity is required only at the unperturbed boundary; the integrand may be discontinuous away from that boundary.

   theorem hasDerivAt_integral_moving_boundary
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : X → ℝ → ℝ} {b B : X → ℝ}
       (hmeas : ∀ h : ℝ, AEStronglyMeasurable
         (fun x => ∫ t in (0 : ℝ)..h * b x, f x t) μ)
       (htrace : AEStronglyMeasurable (fun x => f x 0 * b x) μ)
       (hslice : ∀ᵐ x ∂μ, StronglyMeasurableAtFilter (f x) (nhds 0))
       (hcont : ∀ᵐ x ∂μ, ContinuousAt (f x) 0)
       (hbound : ∀ᵐ x ∂μ, ∀ t : ℝ, ‖f x t‖ ≤ B x)
       (hdom : Integrable (fun x => |b x| * B x) μ) :
       HasDerivAt (fun h : ℝ => ∫ x, (∫ t in (0 : ℝ)..h * b x, f x t) ∂μ)
         (∫ x, f x 0 * b x ∂μ) 0 := by
   …

3. theorem OAI.Problem358.hasDerivAt_integral_moving_boundary_of_measurable line 99

   Source documentation

   A moving-boundary derivative with all measurability discharged from a jointly measurable integrand and a measurable boundary velocity.

   theorem hasDerivAt_integral_moving_boundary_of_measurable
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : X → ℝ → ℝ} {b B : X → ℝ}
       (hf : Measurable (Function.uncurry f)) (hb : Measurable b)
       (hcont : ∀ᵐ x ∂μ, ContinuousAt (f x) 0)
       (hbound : ∀ᵐ x ∂μ, ∀ t : ℝ, ‖f x t‖ ≤ B x)
       (hdom : Integrable (fun x => |b x| * B x) μ) :
       HasDerivAt (fun h : ℝ => ∫ x, (∫ t in (0 : ℝ)..h * b x, f x t) ∂μ)
         (∫ x, f x 0 * b x ∂μ) 0 := by
   …

4. theorem OAI.Problem358.hasDerivAt_integral_moving_boundary_varying line 119

   Source documentation

   A moving-boundary derivative remains valid for a changing integrand. The scaled pointwise limit is exactly what remains after removing the principal moving halfspace in a telescoping product of cell indicators.

   theorem hasDerivAt_integral_moving_boundary_varying
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : ℝ → X → ℝ → ℝ} {b B : X → ℝ} {trace : X → ℝ}
       (hf : ∀ h, Measurable (Function.uncurry (f h))) (hb : Measurable b)
       (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
         Tendsto (fun h : ℝ => f h x (h * u)) (nhds 0) (nhds (trace x)))
       (hbound : ∀ᵐ x ∂μ, ∀ h t : ℝ, ‖f h x t‖ ≤ B x)
       (hdom : Integrable (fun x => |b x| * B x) μ) :
       HasDerivAt (fun h : ℝ => ∫ x, (∫ t in (0 : ℝ)..h * b x, f h x t) ∂μ)
         (∫ x, b x * trace x ∂μ) 0 := by
   …

5. theorem OAI.Problem358.hasDerivAt_integral_moving_boundary_varying_speed line 177

   Source documentation

   A varying boundary velocity is allowed as well. In moving-plane coordinates, this covers the denominator introduced when the normal direction is perturbed.

   theorem hasDerivAt_integral_moving_boundary_varying_speed
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : ℝ → X → ℝ → ℝ} {speed : ℝ → X → ℝ} {A B slope trace : X → ℝ}
       (hf : ∀ h, Measurable (Function.uncurry (f h)))
       (hspeed : ∀ h, Measurable (speed h))
       (hspeedlim : ∀ᵐ x ∂μ, Tendsto (fun h => speed h x) (nhds 0) (nhds (slope x)))
       (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
         Tendsto (fun h : ℝ => f h x (h * speed h x * u)) (nhds 0) (nhds (trace x)))
       (hspeedbound : ∀ᵐ x ∂μ, ∀ h : ℝ, |speed h x| ≤ A x)
       (hbound : ∀ᵐ x ∂μ, ∀ h t : ℝ, ‖f h x t‖ ≤ B x)
       (hdom : Integrable (fun x => A x * B x) μ) :
       HasDerivAt (fun h : ℝ => ∫ x, (∫ t in (0 : ℝ)..h * speed h x, f h x t) ∂μ)
   …

6. theorem OAI.Problem358.integral_threshold_difference line 233

   Source documentation

   The signed change of a threshold halfline is exactly its boundary strip.

   theorem integral_threshold_difference (f : ℝ → ℝ) (c : ℝ) :
       (∫ t : ℝ, f t * ((if c ≤ t then (1 : ℝ) else 0) -
         (if 0 ≤ t then (1 : ℝ) else 0))) = ∫ t in c..0, f t := by
   …

7. theorem OAI.Problem358.hasDerivAt_integral_halfspace_difference line 258

   Source documentation

   The derivative of one varying halfspace factor, with all other varying factors included in f. This is stated as an iterated integral so that an orthogonal-coordinate/Fubini argument can apply it directly.

   theorem hasDerivAt_integral_halfspace_difference
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : ℝ → X → ℝ → ℝ} {speed : ℝ → X → ℝ} {A B slope trace : X → ℝ}
       (hf : ∀ h, Measurable (Function.uncurry (f h)))
       (hspeed : ∀ h, Measurable (speed h))
       (hspeedlim : ∀ᵐ x ∂μ, Tendsto (fun h => speed h x) (nhds 0) (nhds (slope x)))
       (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
         Tendsto (fun h : ℝ => f h x (-(h * speed h x * u))) (nhds 0) (nhds (trace x)))
       (hspeedbound : ∀ᵐ x ∂μ, ∀ h : ℝ, |speed h x| ≤ A x)
       (hbound : ∀ᵐ x ∂μ, ∀ h t : ℝ, ‖f h x t‖ ≤ B x)
       (hdom : Integrable (fun x => A x * B x) μ) :
       HasDerivAt (fun h : ℝ => ∫ x, (∫ t : ℝ,
   …

8. theorem OAI.Problem358.hasDerivAt_integral_halfspace_difference_local line 289

   Source documentation

   Local-in-parameter version of the halfspace derivative. In particular, velocity denominators need only stay away from zero near the base configuration.

   theorem hasDerivAt_integral_halfspace_difference_local
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : ℝ → X → ℝ → ℝ} {speed : ℝ → X → ℝ} {A B slope trace : X → ℝ}
       {s : Set ℝ} (hs : s ∈ nhds 0)
       (hf : ∀ h, Measurable (Function.uncurry (f h)))
       (hspeed : ∀ h, Measurable (speed h))
       (hspeedlim : ∀ᵐ x ∂μ, Tendsto (fun h => speed h x) (nhds 0) (nhds (slope x)))
       (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
         Tendsto (fun h : ℝ => f h x (-(h * speed h x * u))) (nhds 0) (nhds (trace x)))
       (hspeedbound : ∀ᵐ x ∂μ, ∀ h ∈ s, |speed h x| ≤ A x)
       (hbound : ∀ᵐ x ∂μ, ∀ h ∈ s, ∀ t : ℝ, ‖f h x t‖ ≤ B x)
       (hdom : Integrable (fun x => A x * B x) μ) :
   …

9. theorem OAI.Problem358.integrable_threshold_difference line 355

   Source documentation

   Multiplication by the signed difference of two threshold indicators preserves ambient integrability.

   theorem integrable_threshold_difference
       {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {f : X × ℝ → ℝ} {c : X → ℝ}
       (hf : Integrable f (μ.prod volume)) (hc : Measurable c) :
       Integrable (fun p : X × ℝ => f p *
         ((if c p.1 ≤ p.2 then (1 : ℝ) else 0) -
           (if 0 ≤ p.2 then (1 : ℝ) else 0))) (μ.prod volume) := by
   …

10. theorem OAI.Problem358.hasDerivAt_prod_integral_halfspace_difference_local line 383

    Source documentation

    Product-measure version of the local moving-face derivative. Ambient integrability is enough to discharge the Fubini step, while slice domination controls the derivative independently of the parameter.

    theorem hasDerivAt_prod_integral_halfspace_difference_local
        {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
        {f : ℝ → X → ℝ → ℝ} {speed : ℝ → X → ℝ} {A B slope trace : X → ℝ}
        {s : Set ℝ} (hs : s ∈ nhds 0)
        (hf : ∀ h, Measurable (Function.uncurry (f h)))
        (hspeed : ∀ h, Measurable (speed h))
        (hspeedlim : ∀ᵐ x ∂μ, Tendsto (fun h => speed h x) (nhds 0) (nhds (slope x)))
        (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
          Tendsto (fun h : ℝ => f h x (-(h * speed h x * u))) (nhds 0) (nhds (trace x)))
        (hspeedbound : ∀ᵐ x ∂μ, ∀ h ∈ s, |speed h x| ≤ A x)
        (hbound : ∀ᵐ x ∂μ, ∀ h ∈ s, ∀ t : ℝ, ‖f h x t‖ ≤ B x)
        (hdom : Integrable (fun x => A x * B x) μ)
    …