CutVariation.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.hasDerivAt_integral_cut_difference_of_chart line 15

Source documentation

Transport the moving-halfspace derivative through a measure-preserving coordinate chart. The affine geometry enters only through the exact threshold identity, while the derivative and all integration steps are proved here.

theorem hasDerivAt_integral_cut_difference_of_chart
    {X V : Type*} [MeasurableSpace X] [MeasurableSpace V]
    {μ : Measure X} [SFinite μ] {ρ : Measure V}
    {chart : X × ℝ → V} (hchart : MeasurePreserving chart (μ.prod volume) ρ)
    {f ell : ℝ → V → ℝ} {speed : ℝ → X → ℝ} {A B slope trace : X → ℝ}
    {s : Set ℝ} (hs : s ∈ nhds 0)
    (hf : ∀ h, Measurable (f h)) (hell : ∀ h, Measurable (ell h))
    (hspeed : ∀ h, Measurable (speed h))
    (hlevel : ∀ h ∈ s, ∀ p : X × ℝ,
      0 ≤ ell h (chart p) ↔ -(h * speed h p.1) ≤ p.2)
    (hspeedlim : ∀ᵐ x ∂μ, Tendsto (fun h => speed h x) (nhds 0) (nhds (slope x)))
    (hlim : ∀ᵐ x ∂μ, ∀ u : ℝ,
…

theorem OAI.Problem358.FiniteIntersectionVariation.prod_range_sub_prod_range line 75

Source documentation

Exact finite telescoping formula, changing the factors one at a time.

theorem prod_range_sub_prod_range {R : Type*} [CommRing R]
    (a b : ℕ → R) (n : ℕ) :
    (∏ i ∈ Finset.range n, a i) - (∏ i ∈ Finset.range n, b i) =
      ∑ i ∈ Finset.range n,
        (a i - b i) * (∏ j ∈ Finset.range i, a j) *
          ∏ j ∈ Finset.Ico (i + 1) n, b j := by
…

theorem OAI.Problem358.FiniteIntersectionVariation.indicator_finite_intersection line 102

Source documentation

The indicator of a finite intersection factors into the individual indicators.

theorem indicator_finite_intersection {X : Type*} (A : ℕ → Set X) (n : ℕ) (x : X) :
    ({x | ∀ i < n, x ∈ A i}.indicator (fun _ => (1 : ℝ))) x =
      ∏ i ∈ Finset.range n, (A i).indicator (fun _ => (1 : ℝ)) x := by
…

theorem OAI.Problem358.FiniteIntersectionVariation.indicator_intersection_sub line 120

Source documentation

Each term changes one cut; all other cuts appear only as bounded indicator factors.

theorem indicator_intersection_sub {X : Type*} (A B : ℕ → Set X) (n : ℕ) (x : X) :
    ({x | ∀ i < n, x ∈ A i}.indicator (fun _ => (1 : ℝ))) x -
      ({x | ∀ i < n, x ∈ B i}.indicator (fun _ => (1 : ℝ))) x =
    ∑ i ∈ Finset.range n,
      ((A i).indicator (fun _ => (1 : ℝ)) x - (B i).indicator (fun _ => (1 : ℝ)) x) *
        (∏ j ∈ Finset.range i, (A j).indicator (fun _ => (1 : ℝ)) x) *
        ∏ j ∈ Finset.Ico (i + 1) n, (B j).indicator (fun _ => (1 : ℝ)) x := by
…

def OAI.Problem358.FiniteIntersectionVariation.cutTerm line 131
Source documentation
Signed contribution from changing one cut in the finite intersection.
```
def cutTerm {X : Type*} (A B : ℕ → Set X) (n i : ℕ) (x : X) : ℝ :=
…
```
lemma OAI.Problem358.FiniteIntersectionVariation.norm_indicator_one_le line 136
lemma OAI.Problem358.FiniteIntersectionVariation.norm_cutTerm_le line 141
lemma OAI.Problem358.FiniteIntersectionVariation.measurable_cutTerm line 163
lemma OAI.Problem358.FiniteIntersectionVariation.integrable_cutTerm_mul line 174

theorem OAI.Problem358.FiniteIntersectionVariation.integral_indicator_intersection_sub line 182

Source documentation

Weighted integral form of finite-intersection telescoping.

theorem integral_indicator_intersection_sub (A B : ℕ → Set X) (n : ℕ)
    (hA : ∀ j, MeasurableSet (A j)) (hB : ∀ j, MeasurableSet (B j))
    {w : X → ℝ} (hw : Integrable w μ) :
    (∫ x, (({x | ∀ i < n, x ∈ A i}.indicator (fun _ => (1 : ℝ))) x -
        ({x | ∀ i < n, x ∈ B i}.indicator (fun _ => (1 : ℝ))) x) * w x ∂μ) =
      ∑ i ∈ Finset.range n, ∫ x, cutTerm A B n i x * w x ∂μ := by
…

Mentions: OAI.Problem358.FiniteIntersectionVariation.cutTerm

lemma OAI.Problem358.FiniteIntersectionVariation.measurableSet_finiteIntersection line 197

theorem OAI.Problem358.FiniteIntersectionVariation.integral_intersection_sub_integral_intersection line 207

Source documentation

Difference of weighted intersection integrals is the sum of independent cut variations.

theorem integral_intersection_sub_integral_intersection (A B : ℕ → Set X) (n : ℕ)
    (hA : ∀ j, MeasurableSet (A j)) (hB : ∀ j, MeasurableSet (B j))
    {w : X → ℝ} (hw : Integrable w μ) :
    (∫ x in {x | ∀ i < n, x ∈ A i}, w x ∂μ) -
      (∫ x in {x | ∀ i < n, x ∈ B i}, w x ∂μ) =
      ∑ i ∈ Finset.range n, ∫ x, cutTerm A B n i x * w x ∂μ := by
…

Mentions: OAI.Problem358.FiniteIntersectionVariation.cutTerm

theorem OAI.Problem358.FiniteIntersectionVariation.hasDerivAt_intersection_integral line 229

Source documentation

Reassemble derivatives of signed single-cut contributions into the derivative of a cell integral.

theorem hasDerivAt_intersection_integral (A : ℝ → ℕ → Set X) (n : ℕ)
    (hA : ∀ t i, MeasurableSet (A t i)) {w : X → ℝ} (hw : Integrable w μ)
    (d : ℕ → ℝ)
    (hd : ∀ i < n, HasDerivAt
      (fun t : ℝ => ∫ x, cutTerm (A t) (A 0) n i x * w x ∂μ) (d i) 0) :
    HasDerivAt (fun t : ℝ => ∫ x in {x | ∀ i < n, x ∈ A t i}, w x ∂μ)
      (∑ i ∈ Finset.range n, d i) 0 := by
…

Mentions: OAI.Problem358.FiniteIntersectionVariation.cutTerm

lemma OAI.Problem358.FiniteIntersectionVariation.integrable_cutTerm_smul line 251

theorem OAI.Problem358.FiniteIntersectionVariation.integral_intersection_sub_integral_intersection_vector line 259

Source documentation

Vector-valued version, in particular applicable to unnormalized cell moments.

theorem integral_intersection_sub_integral_intersection_vector
    (A B : ℕ → Set X) (n : ℕ)
    (hA : ∀ j, MeasurableSet (A j)) (hB : ∀ j, MeasurableSet (B j))
    {w : X → V} (hw : Integrable w μ) :
    (∫ x in {x | ∀ i < n, x ∈ A i}, w x ∂μ) -
      (∫ x in {x | ∀ i < n, x ∈ B i}, w x ∂μ) =
      ∑ i ∈ Finset.range n, ∫ x, cutTerm A B n i x • w x ∂μ := by
…

Mentions: OAI.Problem358.FiniteIntersectionVariation.cutTerm

theorem OAI.Problem358.FiniteIntersectionVariation.hasDerivAt_intersection_integral_vector line 288

Source documentation

Reassemble single-cut derivatives for vector-valued integrals, including cell moments.

theorem hasDerivAt_intersection_integral_vector (A : ℝ → ℕ → Set X) (n : ℕ)
    (hA : ∀ t i, MeasurableSet (A t i)) {w : X → V} (hw : Integrable w μ)
    (d : ℕ → V)
    (hd : ∀ i < n, HasDerivAt
      (fun t : ℝ => ∫ x, cutTerm (A t) (A 0) n i x • w x ∂μ) (d i) 0) :
    HasDerivAt (fun t : ℝ => ∫ x in {x | ∀ i < n, x ∈ A t i}, w x ∂μ)
      (∑ i ∈ Finset.range n, d i) 0 := by
…

Mentions: OAI.Problem358.FiniteIntersectionVariation.cutTerm

theorem OAI.Problem358.norm_indicator_iInter_sub_le_sum line 322

Source documentation

Changing membership in a finite intersection requires changing membership in at least one cut. This weighted pointwise form also applies to signed moments.

theorem norm_indicator_iInter_sub_le_sum
    {ι X F : Type*} [Fintype ι] [NormedAddCommGroup F]
    (A B : ι → Set X) (f : X → F) (x : X) :
    ‖(⋂ i, A i).indicator f x - (⋂ i, B i).indicator f x‖ ≤
      ∑ i, ‖(A i).indicator f x - (B i).indicator f x‖ := by
…

theorem OAI.Problem358.norm_integral_iInter_sub_le_sum line 356

Source documentation

The total variation of a finite-cut weighted integral is bounded by the sum of the individual weighted cut variations.

theorem norm_integral_iInter_sub_le_sum
    {ι X : Type*} [Fintype ι] [MeasurableSpace X] {μ : Measure X}
    {A B : ι → Set X} {f : X → ℝ}
    (hA : ∀ i, MeasurableSet (A i)) (hB : ∀ i, MeasurableSet (B i))
    (hf : Integrable f μ) :
    ‖(∫ x in ⋂ i, A i, f x ∂μ) - (∫ x in ⋂ i, B i, f x ∂μ)‖ ≤
      ∑ i, ∫ x, ‖(A i).indicator f x - (B i).indicator f x‖ ∂μ := by
…

theorem OAI.Problem358.lipschitzOnWith_integral_iInter_of_cutL1 line 383

Source documentation

Finite intersections preserve quantitative Lipschitz control when each cut is controlled in weighted L¹. No differentiation or nonnegative density premise is assumed, so both cell mass and cell moments fit this interface.

theorem lipschitzOnWith_integral_iInter_of_cutL1
    {ι X A : Type*} [Fintype ι] [MeasurableSpace X] [PseudoMetricSpace A]
    {μ : Measure X} {S : Set A} {cuts : A → ι → Set X} {f : X → ℝ}
    (C : ι → ℝ≥0) (hf : Integrable f μ)
    (hcuts : ∀ a ∈ S, ∀ i, MeasurableSet (cuts a i))
    (hcut : ∀ a ∈ S, ∀ b ∈ S, ∀ i,
      (∫ x, ‖(cuts a i).indicator f x - (cuts b i).indicator f x‖ ∂μ) ≤
        C i * dist a b) :
    LipschitzOnWith (∑ i, C i)
      (fun a => ∫ x in ⋂ i, cuts a i, f x ∂μ) S := by
…

def OAI.Problem358.FiniteCellVariation.remainingIndicator line 416
Source documentation
The unchanged factors in the one-cut-at-a-time expansion of a cell.
```
def remainingIndicator {V : Type*} (ell : ℝ → ℕ → V → ℝ)
    (n i : ℕ) (h : ℝ) (v : V) : ℝ :=
…
```
lemma OAI.Problem358.FiniteCellVariation.norm_remainingIndicator_le line 421
lemma OAI.Problem358.FiniteCellVariation.measurable_remainingIndicator line 435
lemma OAI.Problem358.FiniteCellVariation.integrable_remainingIndicator_mul line 445

theorem OAI.Problem358.FiniteCellVariation.hasDerivAt_cell_integral_of_face_charts line 457

Source documentation

Scalar weighted cell differentiation assembled from measure-preserving face charts. All ambient integrability and finite-intersection algebra are discharged here; the remaining hypotheses are exclusively the local geometry, trace, and domination data of the individual faces. The chart spaces may depend on the face.

theorem hasDerivAt_cell_integral_of_face_charts
    {V : Type*} [MeasurableSpace V] {ρ : Measure V}
    {X : ℕ → Type*} [∀ i, MeasurableSpace (X i)]
    {μ : ∀ i, Measure (X i)} [∀ i, SFinite (μ i)]
    (ell : ℝ → ℕ → V → ℝ) (n : ℕ)
    (hell : ∀ h i, Measurable (ell h i))
    {w : V → ℝ} (hwM : Measurable w) (hw : Integrable w ρ)
    (chart : ∀ i, X i × ℝ → V)
    (hchart : ∀ i < n, MeasurePreserving (chart i) ((μ i).prod volume) ρ)
    (speed : ∀ i, ℝ → X i → ℝ)
    (A B slope trace : ∀ i, X i → ℝ) (s : ℕ → Set ℝ)
    (hs : ∀ i < n, s i ∈ nhds 0)
…