Inverse maps on open sets with global metric bounds

MathlibAnnex.BilipschitzOrientation.BiLipschitzOpenData

structure

Records the maps, their inverse relations, and the quantitative bounds used in the orientation argument.

Statement

Fix and put with the sup norm . The structure specifies open sets and maps . Their restrictions and are inverse bijections. Both maps have global Lipschitz bounds, and has a positive global lower bound.

Definition

Choose as above, constants , and a real number . Require the image and inverse relations and the three metric estimates Thus the upper and lower estimates concern all ambient points. They are additional global requirements; the inverse relations themselves are imposed only on the two open sets.

Assumptions

The dimension may be zero. The sets and are open; neither connectedness, nonemptiness nor finite measure is required. The maps and are defined on all of .

Conclusion

The specified restrictions are inverse bijections between and , with the displayed global bounds available for subsequent arguments. The definition does not require and to be inverse at every point outside those sets.

These are chosen objects together with their stated properties, not an orientation or volume theorem. In particular, the global injectivity of is a consequence of the lower estimate, rather than an additional stored condition.

structure BiLipschitzOpenData (n : ℕ) where
  source : Set (Fin n → ℝ)
  target : Set (Fin n → ℝ)
  isOpen_source : IsOpen source
  isOpen_target : IsOpen target
  f : (Fin n → ℝ) → (Fin n → ℝ)
  g : (Fin n → ℝ) → (Fin n → ℝ)
  mapsTo_f : MapsTo f source target
  mapsTo_g : MapsTo g target source
  left_inv : Set.LeftInvOn g f source
  right_inv : Set.RightInvOn g f target
  fConstant : ℝ≥0
  lipschitzWith_f : LipschitzWith fConstant f
  gConstant : ℝ≥0
  lipschitzWith_g : LipschitzWith gConstant g
  lower : ℝ
  lower_pos : 0 < lower
  anti : ∀ x y, lower * ‖x - y‖ ≤ ‖f x - f y‖

noncomputable section

open Set MeasureTheory Filter
open scoped ENNReal NNReal Topology

namespace MathlibAnnex
namespace BilipschitzOrientation

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project