MovingBoundary.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.MovingBoundary.hasDerivAt_integral_movingEndpoint line 16

Source documentation

A moving integration endpoint in a product-space strip differentiates to the integral on its boundary slice. Only almost-everywhere slice continuity is needed.

theorem hasDerivAt_integral_movingEndpoint
    {f : ℝ → X → ℝ} {c : ℝ} {bound : X → ℝ}
    (hf : StronglyMeasurable (Function.uncurry f))
    (hbound : ∀ᶠ t in 𝓝 c, ∀ᵐ x ∂μ, ‖f t x‖ ≤ bound x)
    (hbound_int : Integrable bound μ)
    (hcont : ∀ᵐ x ∂μ, ContinuousAt (fun t => f t x) c)
    (hint : ∀ᶠ t in 𝓝 c,
      Integrable (Function.uncurry f) ((volume.restrict (uIoc c t)).prod μ)) :
    HasDerivAt (fun t => ∫ x, (∫ s in c..t, f s x) ∂μ)
      (∫ x, f c x ∂μ) c := by
…

theorem OAI.Problem358.MovingBoundary.hasDerivAt_integral_movingEndpoint_of_bound line 42

Source documentation

Global domination in the transverse variable supplies all local strip integrability requirements of the moving-endpoint formula.

theorem hasDerivAt_integral_movingEndpoint_of_bound
    {f : ℝ → X → ℝ} {c : ℝ} {bound : X → ℝ}
    (hf : StronglyMeasurable (Function.uncurry f))
    (hbound : ∀ᵐ x ∂μ, ∀ t, ‖f t x‖ ≤ bound x)
    (hbound_int : Integrable bound μ)
    (hcont : ∀ᵐ x ∂μ, ContinuousAt (fun t => f t x) c) :
    HasDerivAt (fun t => ∫ x, (∫ s in c..t, f s x) ∂μ)
      (∫ x, f c x ∂μ) c := by
…

theorem OAI.Problem358.MovingBoundary.hasDerivAt_integral_movingBoundary line 64

Source documentation

The velocity may vary across the transverse slice. This is the local moving-face formula after straightening a hyperplane and rescaling its normal.

theorem hasDerivAt_integral_movingBoundary
    {f : ℝ → X → ℝ} {v : X → ℝ} {c : ℝ} {bound : X → ℝ}
    (hf : StronglyMeasurable (Function.uncurry f)) (hv : Measurable v)
    (hbound : ∀ᵐ x ∂μ, ∀ t, ‖f t x‖ ≤ bound x)
    (hweighted : Integrable (fun x => |v x| * bound x) μ)
    (hcont : ∀ᵐ x ∂μ, ContinuousAt (fun t => f t x) c) :
    HasDerivAt (fun t => ∫ x, (∫ s in c..(c + t * v x), f s x) ∂μ)
      (∫ x, v x * f c x ∂μ) 0 := by
…

theorem OAI.Problem358.MovingBoundary.hasDerivAt_integral_movingAffineFace line 105

Source documentation

Normal coefficients may also move: solving an affine moving-face equation introduces the scalar factor t / (n + t * k). Its derivative is harmless when n ≠ 0, as required for a genuine initial face normal.

theorem hasDerivAt_integral_movingAffineFace
    {f : ℝ → X → ℝ} {v : X → ℝ} {c n k : ℝ} {bound : X → ℝ}
    (hn : n ≠ 0) (hf : StronglyMeasurable (Function.uncurry f)) (hv : Measurable v)
    (hbound : ∀ᵐ x ∂μ, ∀ t, ‖f t x‖ ≤ bound x)
    (hweighted : Integrable (fun x => |v x| * bound x) μ)
    (hcont : ∀ᵐ x ∂μ, ContinuousAt (fun t => f t x) c) :
    HasDerivAt (fun t => ∫ x,
      (∫ s in c..(c + (t / (n + t * k)) * v x), f s x) ∂μ)
      ((∫ x, v x * f c x ∂μ) / n) 0 := by
…

theorem OAI.Problem358.MovingBoundary.integral_subgraph_eq_iterated line 140

Source documentation

Fubini for a measurable subgraph, with the normal coordinate integrated first.

theorem integral_subgraph_eq_iterated
    {f : ℝ → X → ℝ} {q : X → ℝ}
    (hf : Integrable (Function.uncurry f) (volume.prod μ)) (hq : Measurable q) :
    (∫ p in {p : ℝ × X | p.1 ≤ q p.2}, f p.1 p.2 ∂volume.prod μ) =
      ∫ x, (∫ s in Iic (q x), f s x) ∂μ := by
…

theorem OAI.Problem358.MovingBoundary.integrable_integral_subgraph line 159

Source documentation

The inner subgraph integral is integrable in the transverse coordinate.

theorem integrable_integral_subgraph
    {f : ℝ → X → ℝ} {q : X → ℝ}
    (hf : Integrable (Function.uncurry f) (volume.prod μ)) (hq : Measurable q) :
    Integrable (fun x => ∫ s in Iic (q x), f s x) μ := by
…

theorem OAI.Problem358.MovingBoundary.integral_subgraph_sub line 172

Source documentation

The difference of two subgraph integrals is exactly their oriented strip integral.

theorem integral_subgraph_sub
    {f : ℝ → X → ℝ} {q₀ q₁ : X → ℝ}
    (hf : Integrable (Function.uncurry f) (volume.prod μ))
    (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) :
    (∫ p in {p : ℝ × X | p.1 ≤ q₁ p.2}, f p.1 p.2 ∂volume.prod μ) -
        (∫ p in {p : ℝ × X | p.1 ≤ q₀ p.2}, f p.1 p.2 ∂volume.prod μ) =
      ∫ x, (∫ s in q₀ x..q₁ x, f s x) ∂μ := by
…

theorem OAI.Problem358.MovingBoundary.norm_integral_subgraph_sub_le line 188

Source documentation

An oriented moving strip has the expected absolute integral bound. This estimate needs no boundary continuity and supplies local Lipschitz control.

theorem norm_integral_subgraph_sub_le
    {f : ℝ → X → ℝ} {q₀ q₁ bound : X → ℝ}
    (hf : Integrable (Function.uncurry f) (volume.prod μ))
    (hq₀ : Measurable q₀) (hq₁ : Measurable q₁)
    (hbound : ∀ᵐ x ∂μ, ∀ s, ‖f s x‖ ≤ bound x)
    (hint : Integrable (fun x => bound x * |q₁ x - q₀ x|) μ) :
    ‖(∫ p in {p : ℝ × X | p.1 ≤ q₁ p.2}, f p.1 p.2 ∂volume.prod μ) -
        (∫ p in {p : ℝ × X | p.1 ≤ q₀ p.2}, f p.1 p.2 ∂volume.prod μ)‖ ≤
      ∫ x, bound x * |q₁ x - q₀ x| ∂μ := by
…

theorem OAI.Problem358.MovingBoundary.lipschitzOnWith_integral_subgraph line 205

Source documentation

Lipschitz motion of the threshold gives Lipschitz motion of the subgraph integral. The transverse speed is allowed to vary and is integrated against the density bound, so this applies to affine moving-face charts on compact sources.

theorem lipschitzOnWith_integral_subgraph
    {A : Type*} [PseudoMetricSpace A] {S : Set A} {C : ℝ≥0}
    {f : ℝ → X → ℝ} {q : A → X → ℝ} {bound speed : X → ℝ}
    (hf : Integrable (Function.uncurry f) (volume.prod μ))
    (hq : ∀ a ∈ S, Measurable (q a))
    (hbound : ∀ᵐ x ∂μ, ∀ s, ‖f s x‖ ≤ bound x)
    (hweighted : Integrable (fun x => bound x * speed x) μ)
    (hcost : (∫ x, bound x * speed x ∂μ) ≤ C)
    (hmotion : ∀ a ∈ S, ∀ b ∈ S, ∀ᵐ x ∂μ,
      |q a x - q b x| ≤ speed x * dist a b) :
    LipschitzOnWith C (fun a => ∫ p in {p : ℝ × X | p.1 ≤ q a p.2},
      f p.1 p.2 ∂volume.prod μ) S := by
…

theorem OAI.Problem358.MovingBoundary.hasDerivAt_subgraph_movingAffineFace line 237

Source documentation

A genuine moving-halfspace integral differentiates to its boundary integral. The global integrability assumption is automatic for bounded compactly supported cell densities, while continuity is only required almost everywhere on the initial face.

theorem hasDerivAt_subgraph_movingAffineFace
    {f : ℝ → X → ℝ} {v : X → ℝ} {c n k : ℝ} {bound : X → ℝ}
    (hn : n ≠ 0) (hf : StronglyMeasurable (Function.uncurry f))
    (hfi : Integrable (Function.uncurry f) (volume.prod μ)) (hv : Measurable v)
    (hbound : ∀ᵐ x ∂μ, ∀ t, ‖f t x‖ ≤ bound x)
    (hweighted : Integrable (fun x => |v x| * bound x) μ)
    (hcont : ∀ᵐ x ∂μ, ContinuousAt (fun t => f t x) c) :
    HasDerivAt (fun t => ∫ p in {p : ℝ × X | p.1 ≤ c +
        (t / (n + t * k)) * v p.2}, f p.1 p.2 ∂volume.prod μ)
      ((∫ x, v x * f c x ∂μ) / n) 0 := by
…